proposition: Fact opt_enum_t_sum X Y (P : X -> Prop) (Q : Y -> Prop) : opt_enum_t P -> opt_enum_t Q -> opt_enum_t (fun z : X + Y => match z with inl x => P x | inr y => Q y end).
proof: Proof. intros (f & Hf) (g & Hg). exists (fun n => let (a,b) := surj n in match a with | 0 => match f b with Some x => Some (inl x) | _ => None end | _ => match g b with Some y => Some (inr y) | _ => None end end). intros [ x | y ]. + rewrite Hf; split. * intros (b & Hb). destruct (Hsurj 0 b) as (n & Hn). exists n; rewrite Hn, <- Hb; auto. * intros (n & Hn); revert Hn. destruct (surj n) as ([ | a],b). - case_eq (f b); try discriminate; intros u Hu; inversion 1; exists b; auto. - destruct (g b); discriminate. + rewrite Hg; split. * intros (b & Hb). destruct (Hsurj 1 b) as (n & Hn). exists n; rewrite Hn, <- Hb; auto. * intros (n & Hn); revert Hn. destruct (surj n) as ([ | a],b). - destruct (f b); discriminate. - case_eq (g b); try discriminate; intros u Hu; inversion 1; exists b; auto. 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)