proposition: Lemma CE T phi psi : T ⊢ phi ∧ psi -> T ⊢ phi /\ T ⊢ psi.
proof: Proof. intros H. split. - apply (CE1 H). - apply (CE2 H). Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(FOL.Syntax.Facts FOL.Syntax.Theories) Undecidability(Shared.ListAutomation) Lia