proposition: Lemma prv_T_impl T phi psi : (T ⋄ phi) ⊢T psi -> T ⊢T (phi → psi).
proof: Proof. Proof using HF HP ff p Σ_funcs Σ_preds. intros (A & HA1 & HA2). exists (remove (dec_form _ _ _ _) phi A); split. - intros f [[] % HA1 Hf2] % in_remove; subst; intuition. - eapply II, Weak. 1: apply HA2. transitivity (phi :: A). 1: eauto. intros a [-> | Ha]. + now left. + destruct (dec_form _ _ _ _ a phi) as [->|Hr]. 1:now left. right. now eapply in_in_remove. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts