proposition: Lemma tmap_contains_L (f : @form Σ_funcs1 Σ_preds1 ops1 ff1 -> @form Σ_funcs2 Σ_preds2 ops2 ff2) T A : contains_L A (tmap f T) -> exists B, A = List.map f B /\ contains_L B T.
proof: Proof. induction A. - intros. now exists List.nil. - intros H. destruct IHA as (B & -> & HB). 1: firstorder. destruct (H a (or_introl eq_refl)) as (b & Hb & <-). exists (b :: B). split. 1: auto. intros ? []; subst; auto. 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