proposition: Lemma even_ev : forall n: nat, even n = true -> ev n.
proof: Proof. induction n; intros. - apply ev_0. - destruct n. + simpl in H. inversion H. + simpl in H. apply ev_SS. Abort. Definition nat_ind2 : forall (P : nat -> Prop), P 0 -> P 1 -> (forall n : nat, P n -> P (S(S n))) -> forall n : nat , P n := fun P => fun P0 => fun P1 => fun PSS => fix f (n:nat) := match n with 0 => P0 | 1 => P1 | S (S n') => PSS n' (f n') end. Lemma even_ev : forall n, even n = true -> ev n. Proof. intros. induction n as [ | |n'] using nat_ind2. - apply ev_0. - simpl in H. inversion H. - simpl in H. apply ev_SS. apply IHn'. apply H. Qed.