The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

Hello,

I have a proof with a lot of hypotheses of the form X=Y. I already completed
the proof, but it is a lot of typing. At the moment, I manually look for a
maching hypthesis, and then rewrite the goal. The proof then looks like this:

rewrite H0.
rewrite H13.
rewrite H5.
(* Rest of the Proof *)

I tried to use [congruence] to solve my proof. However, this is only possible
if the proof is completed by rewrites. What I'd like to do is apply all
hypothesis with [rewrite] (the local assumptions, and maybe a couple of other
"external" theorems, until none of them is possible anymore. Is there a way to
do this (maybe with Ltac)?

Sincerely