proposition: Lemma imodel_dne (v : vec term (ar_preds P)) : ~ ksat true (fun _ => tt) (¬¬(atom P v) → (atom P v)).
proof: Proof. cbn. intros H. apply (H true); trivial. intros [] _; trivial. intros H'. now apply (H' false). Qed.
imports: Undecidability(FOL.Semantics.Kripke.FragmentCore FOL.Deduction.FragmentND) Undecidability(Shared.ListAutomation)