proposition: Lemma NUM_REP_S i : NUM_REP i -> NUM_REP (IND_SUC i).
proof: Proof. rewrite NUM_REP_eq. intros hi P [h0 hS]. apply hS. apply hi. split. exact h0. exact hS. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts