proposition: Fact opt_enum_rec_enum_discrete P : opt_enum P -> rec_enum P.
proof: Proof. Proof using Xdiscr. intros (f & Hf). exists (fun n x => match f n with Some y => if Xdiscr x y then true else false | None => false end); intros x; rewrite Hf; split. + intros (n & Hn); exists n; rewrite <- Hn. destruct (Xdiscr x x) as [ | [] ]; auto. + intros (n & Hn); revert Hn. case_eq (f n). * intros y Hy. destruct (Xdiscr x y) as [ -> | ]. - exists n; auto. - discriminate. * discriminate. Qed.
imports: List Arith Bool Lia Eqdep_dec Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.Synthetic.InformativeDefinitions Undecidability.Synthetic.InformativeReducibilityFacts Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops decidable)