proposition: Theorem evSS_ev : forall n, ev (S (S n)) -> ev n.
proof: Proof. intros n E. destruct E as [| n' E']. - Abort. Theorem evSS_ev : forall n, ev (S (S n)) -> ev n. Proof. intros n E. inversion E as [| n' E']. apply E'. Qed.
imports: Logic