The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Nice proof, I didn't know about generalize_eqs_vars !

You should mention that this proof introduces an axiom about JMeq:

JMeq_eq : forall (A : Type) (x y : A), JMeq x y -> x = y

V.

Le 24 février 2012 11:07, Pierre Courtieu 
<Pierre.Courtieu AT cnam.fr>
 a écrit :
> Hello, here is a script proving your goal in v8.3 and v8.4 (14975). It
> makes use of JMeq but the statement of the lemma is the one you want.
>
> Tactic dependent generalize_eqs_vars does not seem to be documented
> but one should be able to do the same by hand.
>
> Bests
> P.C.
> ------------8X-------------------
> Require Export JMeq.
>
> Variable A:Type.
> Variable F: A -> A.
> Inductive graF : A -> A -> Type := io_pair (a:A) : graF a (F a).
>
> Goal forall (a:A) (g: graF a (F a)), g = (io_pair a).
> intros a g.
> dependent generalize_eqs_vars g.
> intros g0 H H0.
> induction g.
> apply JMeq_eq.
> auto.
> Qed.