The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

> > > Yet all of this are provable in 8.3:
> > > exists a : Set,a=True:Prop. 
> > > exists a : Prop,a=True:Prop. 
> > > exists! a : Type, a=True:Prop.
> > > 
> > > Is [Prop=Set] in 8.3 too ?
> > > 
> > > Definition FA := True:Prop.
> > > 
> > > Lemma set0: exists a : Set,a=FA.
> > > eexists. firstorder.
> > > Qed.
> > > 
> > > Lemma prop0: exists a : Prop,a=FA.
> > > eexists. firstorder.
> > > Qed.
> > > 
> > > Lemma typeuniq: exists! a : Type, a=FA.
> > > eexists. firstorder.
> > > Qed.
> > 
> > These ones are harmless.
> 
> I am somewhat confused by the unique lemma. Is True:Prop = True:Set - I
> can't formulate it as a lemma. If they are different the unique maybe
> incorrect.

The uniqueness is modulo conversion and "casts" (i.e. the ability to
add a type constraint such as ":Prop") are transparent for conversion,
so we have True:Prop = True = True:Set (where = is the basic
beta-delta-iota-zeta conversion, that in practise also includes cast
removal).

This being said, what conversion actually is does not matter in your
case.  As a matter of fact, if you can prove "exists a, a = t", then
you can systematically prove also "exists! a, a = t".

If what puzzles you is that you compare elements that look to be in
different types, then observe that by subtyping of Prop and Set in
(any of the) Type, True:Prop and True:Set actually have a common
supertype (you can check it by using "Set Printing All" and observe
what the first argument of "eq" is).

Hugo Herbelin