proposition: Lemma IND_SUC_ex : exists f, IND_SUC_pred f.
proof: Proof. destruct axiom_6 as [f [h1 h2]]. exists f. unfold ONTO in h2. rewrite not_forall_eq in h2. destruct h2 as [z h2]. exists z. split. intros x y. apply prop_ext. apply h1. intro e. rewrite e. reflexivity. rewrite not_exists_eq in h2. intros x e. apply (h2 x). symmetry. exact e. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts