The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 04.10.2012 16:45, schrieb Lucian M. Patcas:

You could use rewrite to complete the proof:

  intros X x y P H H0.
  rewrite <- H0 in H.
  assumption.

Lucian

On Thu, Oct 4, 2012 at 9:54 AM, Jonas Oberhauser <s9joober AT gmail.com> wrote:
Hi all,

is there such a thing like a replace at?

  Goal forall X (x y : X) P, P x y -> x = y -> P x x.
  intros.
  replace x with y at 2. (* doesn't work ? *)
  rewrite H at 2. (* supposedly requries Setoid ? *)


replace is too eager.
I have fallen back to:

  pattern x at 2.
  replace x with y.

Kind regards,

jonas

The simplicity of my example implied the viability of such a solution which is not given in the situation I was facing in reality.
Kind regards, jonas.