proposition: Lemma ksat_mon {ff : falsity_flag} (u : nodes) (rho : nat -> domain) (phi : form) : forall v (H : reachable u v), ksat u rho phi -> ksat v rho phi.
proof: Proof. revert rho. induction phi; intros rho v' H; cbn; try destruct b0; try destruct q; intuition; eauto using mon_P, reach_tran. Qed.
imports: Undecidability.FOL.Semantics.Tarski.FragmentFacts Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability.FOL.Syntax.Facts Undecidability(Shared.ListAutomation)