proposition: Lemma appCtx b psi1 psi2 A : In (psi1 → psi2) A -> A ⊢I psi1 -> A ⊢I psi2.
proof: Proof. intros. eapply (IE (phi := psi1) (psi := psi2)); eauto using Ctx. Qed.
imports: Undecidability.PCP(PCP Util.PCP_facts) Undecidability.FOL(Deduction.FragmentNDFacts Semantics.Tarski.FragmentFacts Semantics.Tarski.FragmentSoundness Syntax.Core Syntax.Facts) Undecidability.FOL(FOL) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ReducibilityFacts MoreReducibilityFacts) Undecidability.FOL.Reductions.PCPb_to_FOL Undecidability.PCP.Reductions.PCPb_iff_dPCPb List Undecidability(Shared.ListAutomation)