Section Coucou.

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

  Lemma fg_ok : f 4 = g 6.
  apply fg.
  Qed.

  Hypothesis gf : forall x, g (x+2) = f x.
  Lemma gf_wrong : g 6 = f 4.
  apply gf.
(* Error! *)


  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 prz2 : g 4 = f 4 -> g 4 = g 6.
  intro. 
  specialize trans with (y:=f 4).
  (* it should either work! (would be best ;) 
      or signal an error, not silently do nothing *)