proposition: Lemma XM A (phi : form) : A ⊢C (phi ∨ ¬ phi).
proof: Proof. apply (@XMc _ phi). - apply DI1, Ctx. now left. - apply DI2, Ctx. now left. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(FOL.Syntax.Facts FOL.Syntax.Theories) Undecidability(Shared.ListAutomation) Lia