The Coq mailing list

[Pierre-Yves Strub <pierre-yves AT strub.nu>]

You proved:

False -> Q and False -> ~Q

because VAR is discharged when you close the section.

Pierre-Yves.

On Fri, 24 Jun 2011 16:35:43 +0300, Georgi Guninski wrote:

> i am somewhat surprised why you don't print False->stuff here:
>
> Section S.
> Lemma T : Prop.
> exact False.
> Defined.
>
> Variable VAR : T.
>
> Lemma L_2: exists a : T, a = VAR.
> eexists. instantiate (1:=VAR). reflexivity.
> Defined.
>
>
> Lemma L_1: ~(exists a : T, a = VAR).
>
> change ((exists a : T, a = VAR) -> False); intro H; refine (ex_ind _ 
> H);
>        clear H; intro x; intro H; auto with *.
> Defined.
>
> End S.