proposition: Lemma SUC_def : S = (fun _2104 : nat => mk_num (IND_SUC (dest_num _2104))).
proof: Proof. symmetry. apply fun_ext; intro x. rewrite mk_num_S. 2: apply NUM_REP_dest_num. apply f_equal. apply axiom_7. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts