The Coq mailing list

["Lucian M. Patcas" <lucian.patcas AT gmail.com>]

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