The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Ian Lynagh wrote:
> Lemma Lem : forall (x : nat), (x = 3).
> Proof.
> intros.
> assert (forall (y : nat), (x = y) ->
>          forall (z : nat), (x = z) ->  (x = 3)).
>      admit.
>
> (* 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.