Inductive wrong_ev (m:nat) : Prop :=
| wrong_ev_0 : wrong_ev 0 -> wrong_ev m
| wrong_ev_SS : forall n, wrong_ev n -> wrong_ev (S (S n)) -> wrong_ev m.

Theorem nonsense : forall n (e:wrong_ev n), False.
Proof.
  intros n H.
  induction H.
  apply IHwrong_ev.
  apply IHwrong_ev1.
Qed.