proposition: Lemma enum_tmap' (f : @form Σ_funcs1 Σ_preds1 ops1 ff1 -> @form Σ_funcs2 Σ_preds2 ops2 ff2) (T : @theory Σ_funcs1 Σ_preds1 ops1 ff1) L : cumulative L -> list_enumerator L T -> cumulative (L >> List.map f) /\ list_enumerator (L >> List.map f) (tmap f T).
proof: Proof. intros H H0. split; unfold ">>". - intros n. destruct (H n) as [A ->]. exists (List.map f A). apply map_app. - intros x; split. + intros (phi & [m Hin] % H0 & <-). exists m. apply in_map_iff. firstorder. + intros (m & (phi & <- & Hphi) % in_map_iff). firstorder. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation) Undecidability(Shared.Libs.PSL.Vectors.Vectors) Coq.Setoids.Setoid Arith Lia List