proposition: Lemma tmap_closed (f : @form Σ_funcs1 Σ_preds1 ops1 ff1 -> @form Σ_funcs2 Σ_preds2 ops2 ff2) T : (forall x, closed x -> closed (f x)) -> closed_T T -> closed_T (tmap f T).
proof: Proof. intros Hf Hclosed ? (y & Hy & <-). apply Hf, Hclosed, Hy. 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