proposition: Lemma NUM_REP_eq : NUM_REP = NUM_REP'.
proof: Proof. apply fun_ext; intro a. apply prop_ext; intros h P. intros [p0 ps]. apply h. intros a' [i|i]. subst a'. exact p0. destruct i as [b [e i]]. subst a'. apply ps. exact i. intro i. apply h. split. apply i. left. reflexivity. intros b pb. apply i. right. exists b. split. reflexivity. exact pb. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts