include "Nat/defs.ma".
-theorem eq_gen_zero_succ: \forall (P:Prop). \forall m2. zero = succ m2 \to P.
+theorem eq_gen_zero_succ: \forall m2. zero = succ m2 \to False.
intros. destruct H.
qed.
-theorem eq_gen_succ_zero: \forall (P:Prop). \forall m1. succ m1 = zero \to P.
+theorem eq_gen_succ_zero: \forall m1. succ m1 = zero \to False.
intros. destruct H.
qed.