false.elim

Stream: general

[Kenny Lau]

Why can false elim to anything even though it is only a Prop?

[Chris Hughes]

More or less because even if it wasn't a Prop it would still be a subsingleton. Same reason for and eq and acc. I think more precisely any constructors whose type is not a Prop have to be mentioned in the type of the Prop. So acc is okay, because it's non-Prop constructor is mentioned in the type.