proposition: Theorem silly_ex : forall p, (forall n, even n = true -> even (S n) = false) -> (forall n, even n = false -> odd n = true) -> even p = true -> odd (S p) = true.
proof: Proof. Admitted. Theorem silly3 : forall (n m : nat), n = m -> m = n. Proof. intros n m H. Fail apply H. symmetry. apply H. Qed.