The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

Hi,

...
> a : q0_type
> A : Trm (Fun x1 x0)
> H8 : a = Fun x1 x0
> H10 : Fun x1 x0 = s
> H12 : existS (fun x : q0_type => Trm x) (Fun x1 x0) A =
>        existS (fun x : q0_type => Trm x) (Fun x1 x0) (Lambda x2 x3)
> H13 : Fun x1 x0 = s
> H14 : existS (fun x : q0_type => Trm x) (Fun x1 x0) A =
>        existS (fun x : q0_type => Trm x) (Fun x1 x0) (Apply M N)
> ------------------------------------------------------------------- 
> (1/2)
> Logic.False
>
> I am currently clueless as to how to proceed from here.  In  
> particular,  it would be helpful if I knew what the "existS"  
> construct means and how I can make use of the hypotheses invoving  
> it.  I have looked in Coq'Art but cannot seem to find a answer to  
> this question.


Just do "Print existS". Actually it is the single constructor of SigS  
which is a pair of two objects of kind Set, but where the type of the  
second component depends upon the value of the first. There used to  
be some concrete syntax like {x:A|P} for it, but for some reason it  
seems switched off.

Anyway, since existS is a constructor, the first equality implies  
that A=Apply M N, which, I imagine is false.
So inversion H14 should make it.

Cheers,


Benjamin