Section Specialize.

  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). 

  (* specialize *)
  Lemma prz4 : g 4 = f 4 -> g 4 = g 6.
  intro.
  specialize trans with  (x:=g 4) (y:=f 4).
  apply trans.
  assumption.
  change 6 with (4+2). 
  apply fg.
  Qed.