The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

OK, I see now how to do this: you have to generalize over the dependent 
terms and then rewrite and then use the "eq_rec_eq" axiom.

Now, another question: Is it possible to prove that
  (x:A)(D:x=x) D==(refl_equal A x)
from the Eqdep library as it is? If not, has it been shown that adding 
this as an axiom is safe? Can this replace the eq_rec_eq axiom in Eqdep?

Thanks for any help on these issues,
--- nadeem

Require Eqdep.

Variable i:nat.
Variable Fty:nat->Set.
Variable F:(Fty i).
Variable R:(i:?)(Fty i) -> bool.
Variable D:i=O.

Lemma eqR_F : (R i F)=(R O (eq_rec ? i ? F ? D)).
Generalize F.
Generalize D.
Rewrite D.
Intros.
Replace (eq_rec nat O Fty f O e) with f; Auto.
Apply eq_rec_eq.
Save.






Nadeem Abdul Hamid wrote:

> Hello all,
> Is it possible to prove the following at all (i.e. using the Eqdep 
> library):
>
>
> Variable i:nat.
> Variable Fty:nat->Set.
> Variable F:(Fty i).
> Variable R:(i:?)(Fty i) -> bool.
> Variable D:i=O.
>
> Lemma eqR_F : (R i F)=(R O (eq_rec ? i ? F ? D)).
>
>
> Thanks,
> --- nadeem
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club