The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Is there a version of the dependent destruction tactic
that does not use the JMeq_eq axiom?

Section 10.5 of CPDT says that JMeq_eq is derivable
from UIP_refl.
Also, UIP_refl is derivable for types with decidable equality.
http://coq.inria.fr/distrib/8.4/stdlib/Coq.Logic.Eqdep_dec.html

 
A version of dependent destruction could either take the equality decider
explicitly as input, or appeal to a designated hint database
to get the required proofs of decidable equality.

If someone has already written such a tactic and can share the code,
I'd be grateful.

Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/