proposition: Lemma NUM_REP_eq_ID : NUM_REP = NUM_REP_ID.
proof: Proof. apply fun_ext; intro i. apply prop_ext. rewrite NUM_REP_eq. intro h. apply h. split. apply NUM_REP_ID_0. intros j hj. apply NUM_REP_ID_S. exact hj. induction 1. apply NUM_REP_0. apply NUM_REP_S. assumption. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts