proposition: Lemma switch_conj_imp alpha beta phi A : A ⊢ alpha ∧ beta → phi <-> A ⊢ alpha → beta → phi.
proof: Proof. split; intros H. - apply II, II. eapply IE. apply (@Weak A). apply H. firstorder. apply CI; apply Ctx; firstorder. - apply II. eapply IE. eapply IE. eapply Weak. apply H. firstorder. eapply CE1, Ctx; firstorder. eapply CE2, Ctx; firstorder. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(FOL.Syntax.Facts FOL.Syntax.Theories) Undecidability(Shared.ListAutomation) Lia