proposition: Lemma dest_num_inj : ONE_ONE dest_num.
proof: Proof. intro x. induction x; intro y; destruct y; simpl. reflexivity. intro e. apply False_ind. eapply IND_SUC_neq_0. symmetry. exact e. intro e. apply False_ind. eapply IND_SUC_neq_0. exact e. intro e. apply f_equal. apply IHx. apply IND_SUC_inj. exact e. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts