proposition: Lemma prv_T_remove T phi psi : T ⊢T phi -> T ⋄ phi ⊢T psi -> T ⊢T psi.
proof: Proof. Proof using HF HP ff p Σ_funcs Σ_preds. intros (A & HA1 & HA2) (B & HB1 & HB2) % prv_T_impl. use_theory (A ++ B). - now intros psi1 [H1|H2]%in_app_iff; [apply HA1 | apply HB1]. - eapply IE; eapply Weak. 1,3: eassumption. all: intros x Hx; apply in_app_iff; eauto. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts