proposition: Lemma closed_T_extend T phi : closed_T T -> closed phi -> closed_T (T ⋄ phi).
proof: Proof. intros ? ? ? [|]; subst; auto with contains_theory. 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