proposition: Lemma ksoundness'_bot {ff1 ff2 : falsity_flag} (psi : @form _ _ _ ff1) (phi : @form _ _ _ ff2) : closed psi -> (forall xi, kvalid (psi → xi)) -> [] ⊢I phi -> kvalid (phi[psi/⊥]).
proof: Proof. intros Hcl Hexp H % (ksoundness_bot Hcl Hexp). intros D M u rho. now apply (H D M u rho). Qed.
imports: Undecidability(FOL.Semantics.Kripke.FragmentCore FOL.Deduction.FragmentND) Undecidability(Shared.ListAutomation)