proposition: Lemma kvalid_valid b (phi : form b) : kvalid phi -> valid phi.
proof: Proof. intros H domain I rho. apply kripke_tarski, H. Qed.
imports: Undecidability(FOL.Semantics.Tarski.FragmentFacts) Undecidability(FOL.Semantics.Kripke.FragmentCore) Undecidability(Shared.ListAutomation)