proposition: Fact opt_enum_t_image X Y (P : X -> Prop) (Q : Y -> Prop) (f : X -> Y) : (forall y, Q y <-> exists x, P x /\ y = f x) -> opt_enum_t P -> opt_enum_t Q.
proof: Proof. intros Hf (g & Hg). exists (fun n => match g n with Some x => Some (f x) | _ => None end). intros y; rewrite Hf; split. + intros (x & H1 & ->); revert H1; rewrite Hg. intros (n & E); exists n; rewrite <- E; auto. + intros (n & Hn); revert Hn. case_eq (g n); try discriminate. intros x E; inversion 1; exists x; split; auto. apply Hg; exists n; 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)