proposition: Lemma consistent : ~ ([] ⊢ ⊥).
proof: Proof. intros H. unshelve eapply (sound_for_classical_model _ H). - exact (fun _ => tt). - apply TM_sat_decidable. - easy. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories) Undecidability(Shared.ListAutomation) Lia