proposition: Lemma DE' A phi : A ⊢ phi ∨ phi -> A ⊢ phi.
proof: Proof. intros H. apply (DE H); auto. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(FOL.Syntax.Facts FOL.Syntax.Theories) Undecidability(Shared.ListAutomation) Lia