The Coq mailing list

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

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