proposition: Lemma XMc A (phi chi : form) : (phi::A) ⊢C chi -> ((¬ phi)::A) ⊢C chi -> A ⊢C chi.
proof: Proof. intros HA HB. eapply IE with ((phi → chi) → (¬phi → chi) → chi). - eapply II. eapply IE. 1: eapply IE. 1: apply Ctx; now left. 1-2: eapply Weak; [eapply II|]. 1: apply HA. 2: apply HB. 1-2: intros a Ha; now right. - eapply DN. apply II. eapply IE. 1: apply Ctx; now left. eapply II. eapply II. eapply IE. 1: apply Ctx; now left. eapply II. eapply IE. 1: apply Ctx; do 3 right; now left. do 2 eapply II. eapply IE. 1: apply Ctx; right; now left. apply Ctx; now eauto. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts