Section AssertCut.
  Parameter P Q : nat -> Prop.

  Hypothesis pq1: forall n, P n -> Q (S n).

  Lemma q : P 4 -> (forall m, Q m <-> Q (S m)) -> Q 4.
  intros.
  assert (Q 5).
  apply pq1.
  assumption.
(*  apply <- H0.
  assumption. *)
  assert (Q 4 <-> Q 5).
  apply H0.
  destruct H2.
  info auto.
  Qed.
  
  Lemma q1 : P 4 -> (forall m, Q m <-> Q (S m)) -> Q 4.
  intros.
  cut (Q 5).
  cut (Q 4 <-> Q 5).
  intros.
  destruct H1.
  info auto.
  info auto.
  info auto.
  Qed.
  
  Lemma q2 : P 4 -> (forall m, Q m <-> Q (S m)) -> Q 4.
  intros.
  specialize (H0 4).
  destruct H0.
  auto.
  Qed.