proposition: Lemma ksatis_satis b (phi : form b) : satis phi -> ksatis phi.
proof: Proof. intros (domain & I & rho & ?). eapply kripke_tarski in H. now exists domain, (interp_kripke I), tt, rho. Qed.
imports: Undecidability(FOL.Semantics.Tarski.FragmentFacts) Undecidability(FOL.Semantics.Kripke.FragmentCore) Undecidability(Shared.ListAutomation)