proposition: Lemma iprv_dne (v : vec term (ar_preds P)) : ~ [] ⊢I (¬¬(atom P v) → (atom P v)).
proof: Proof. intros H % ksoundness. apply (@imodel_dne v). apply H. intros phi []. Qed.
imports: Undecidability(FOL.Semantics.Kripke.FragmentCore FOL.Deduction.FragmentND) Undecidability(Shared.ListAutomation)