proposition: Theorem bi_rec_enum_t_dec : { P x } + { ~ P x }.
proof: Proof. Proof using Hx H2 H1. destruct H1 as (f & Hf). destruct H2 as (g & Hg). set (h n := f n x = true \/ g n x = true). destruct min_dec with (P := h) as (n & G1 & _). + intro n; unfold h; destruct (f n x); destruct (g n x); auto. right; intros []; discriminate. + destruct Hx as [ H | H ]; revert H. * rewrite Hf; intros (n & Hn); exists n; left; auto. * rewrite Hg; intros (n & Hn); exists n; right; auto. + red in G1. case_eq (f n x). * intros; left; apply Hf; exists n; auto. * intros; right; apply Hg; exists n. rewrite H in G1; destruct G1; auto; 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)