proposition: Lemma ksat_iff {ff : falsity_flag} u rho phi : ksat u rho phi <-> forall v (H : reachable u v), ksat v rho phi.
proof: Proof. split. - intros H1 v H2. eapply ksat_mon; eauto. - intros H. apply H. eapply reach_refl. Qed.
imports: Undecidability.FOL.Semantics.Tarski.FragmentFacts Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability.FOL.Syntax.Facts Undecidability(Shared.ListAutomation)