The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

For the case of a decidable predicate, another workaround is to
rewrite it using a transparent decision procedure.  For example,
something like (untested):

Definition normalize_eq_nat {m n:nat} (e:m=n) : m=n :=
match eq_nat_dec m n with
| left e' => e'
| right ne => False_ind (ne e)
end.

(Apologies to whoever is due credit on this one, I forgot who it was
that posted this trick before.)
-- 
Daniel Schepler