proposition: Lemma sat_bot_False {ff:falsity_flag} u rho phi (e : forall u v, reachable u v -> False -> False) : @ksat_bot ff (fun _ => False) e u rho phi <-> @ksat _ _ domain M ff u rho phi.
proof: Proof. induction phi in rho,u|-*. - easy. - easy. - destruct b0. unfold sat_bot, falsity_to_pred in *. cbn. split; intros H v Hreach H1 %IHphi1; apply IHphi2; now apply H, H1. - destruct q. unfold sat_bot, falsity_to_pred in *. cbn. split; intros H d; apply IHphi, H. Qed.
imports: Undecidability.FOL.Semantics.Tarski.FragmentFacts Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability.FOL.Syntax.Facts Undecidability(Shared.ListAutomation)