proposition: Lemma ksoundness' (phi : form) : [] ⊢I phi -> kvalid phi.
proof: Proof. intros H % ksoundness. intros D I u rho; now eapply H. Qed.
imports: Undecidability(FOL.Semantics.Kripke.FragmentCore FOL.Deduction.FragmentND) Undecidability(Shared.ListAutomation)