The Coq mailing list

["Carlos.SIMPSON" <carlos AT math1.unice.fr>]

Hi. Perhaps I am not following the discussion well enough so maybe somebody 
already said this, but
here is a proof of something which seems to be what you are asking for (???). 
It uses False_rect.
---Carlos Simpson

Implicit Arguments On.

Inductive option [T:Type] : Type :=
none : (option T) |
some : T -> (option T).

Definition is_none :(T:Type)(option T) -> Prop.
Intros.
NewInduction X.
Exact True.
Exact False.
Defined.

Definition really : (T:Type; x:(option T))Prop
:= [T:Type; x:(option T)](ExT [t:T](some t) == x).


Definition null_case : (T:Type)(really (none T)) -> T.
Intros.
Unfold really in H.
Assert False.
NewInduction H.
Assert False == True.
Transitivity (is_none (some x)).
Trivial.
Rewrite H.
Trivial.
Rewrite H0.
Trivial.
Elim H0.
Defined.


Definition constr : (T : Type; x: (option T))(really x) -> T.
Intros.
NewInduction x.
Apply null_case.
Assumption.
Exact t.
Defined.

Lemma lem1 : (T:Type; t:T)(really (some t)).
Intros.
Unfold really.
EApply exT_intro.
Trivial.
Save.

Lemma lem2 : (T:Type; t:T; hyp : (really (some t)))(constr hyp) == t.
Intros.
Trivial.
Save.