Section W.
  Hypothesis trans: forall x y z:nat, x=y -> y=z -> x=z.

  Variable f g : nat -> nat.
  Hypothesis fg : forall x, f x = g (x+2). 


  Lemma prz3 : g 4 = f 4 -> g 4 = g 6.
(*  eauto. *)
  intro.
  eapply trans; info auto.
  
  eapply trans; eauto.

  eassumption.
  change 6 with (4+2). 
  apply fg.
  Qed.