proposition: Lemma sat_bot_False {ff:falsity_flag} rho phi : sat_bot False rho phi <-> sat rho phi.
proof: Proof. induction phi in rho|-*. - easy. - easy. - destruct b0. unfold sat_bot, falsity_to_pred in *. cbn. split; intros H H1 %IHphi1; apply IHphi2; apply H, H1. - destruct q. unfold sat_bot, falsity_to_pred in *. cbn. split; intros H d; apply IHphi, H. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Theories Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability(Shared.ListAutomation) Vector Lia