The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 10/03/2016 18:09, Jacques-Henri Jourdan wrote:
> If I remember correctly, this restriction is important to soundness :
> because Prop is impredicative, we can build a proof of false from
> inhabited T -> T.

I'm not sure this is sufficient. IIRC, you need to assume in addition
that this function is the inverse of the inhabits constructor, otherwise
you won't be able to do much with this function alone.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature