The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

(* Suppose we are here, "nat"s can be shown to exist, and "x = y"
   and "x = z" are provable (we'll just pretend and use admit).
   How can we write this proof without writing "nat" or "x = y"?
   (in a real proof, "nat" and "x = y" would be large expressions I don't
   want to have to repeat) *) 

I don't know if your underlying question has some deeper aspect to it, but [eauto] solves the remaining subgoal here.  If that doesn't work in your real case, then I, at least, would need an example that better exposes the key difficulties.

  Another possible hint may be that one can often avoid writing large expressions occurring in the goal, by using Ltac's possibly of matching on the goal (and hypotheses).

  Adam

-- 
Adam Koprowski   [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate    [http://mlstate.com, 15 rue Berlier, 75013 Paris, France]