proposition: Lemma NUM_REP_eq_dest_num_img : NUM_REP = dest_num_img.
proof: Proof. apply fun_ext; intro i. apply prop_ext. rewrite NUM_REP_eq_ID. revert i. induction 1. exists 0. reflexivity. destruct IHNUM_REP_ID as [n hn]. rewrite hn. exists (S n). reflexivity. intros [n hn]. subst. induction n. apply NUM_REP_0. apply NUM_REP_S. assumption. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts