Section Apply.

  Variable P Q : nat -> Prop.
  
  Hypothesis pq : forall x, P x -> Q x.

  Lemma prz : P 0 -> Q 0.
  intro.
  apply pq.
  Show Proof.
  assumption.
  Qed.

  

  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. (*
  apply pq.
  apply trans.
  apply trans with (f 4).
  apply trans with (y:=f 4). *)
  apply (trans _ (f 4)).
  apply H.
  
  change 6 with (4+2). 
  apply fg.
  Qed.
  
  Lemma prz3 : g 4 = f 4 -> g 4 = g 6.
  intro.
  eapply trans.
  eassumption.
  change 6 with (4+2). 
  apply fg.
  Qed.


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