proposition: Lemma consistent_ND : ~ ([] ⊢ ⊥).
proof: Proof. intros H. unshelve eapply (sound_for_classical_model _ H). - exact (fun _ => tt). - intros rho phi psi. cbn. destruct (TM_sat_decidable rho phi) as [Hl1|Hr1], (TM_sat_decidable rho psi) as [Hl2|Hr2]; tauto. - easy. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories) Undecidability(Shared.ListAutomation) Lia