proposition: Lemma kripke_tarski {ff : falsity_flag} domain (I : interp domain) rho phi : rho ⊨ phi <-> ksat (interp_kripke I) tt rho phi.
proof: Proof. revert rho. induction phi; intros rho. - tauto. - tauto. - destruct b0. cbn. rewrite IHphi1, IHphi2. intuition. destruct v. tauto. - destruct q. cbn. split; intros H; cbn in *. + intros i. apply IHphi, H. + intros i. apply IHphi, H. Qed.
imports: Undecidability(FOL.Semantics.Tarski.FragmentFacts) Undecidability(FOL.Semantics.Kripke.FragmentCore) Undecidability(Shared.ListAutomation)