The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Hi,

Can somebody tell me what is a usually solution for situation when Coq
automatically rewrite variable, but I need to rewrite these variable after
that, with some hypotheses introduced in environment before using opening
proof mode.
For example:

Coq < Section Proba.

Coq < Parameter x y : nat.
x is assumed
y is assumed

Coq < Goal exists y, x=y.
1 subgoal

  ============================
   exists y0 : nat, x = y0

So, I like to have hypotheses for rewriting but I cannot using name y0
because than Coq will rewrite y in some another name. Introducing new
hypotheses using tactics after Coq's rewriting don't look so elegant.

Thank you very much,

Marko Malikoviæ