proposition: Corollary sat_closed {ff : falsity_flag} rho sigma phi : bounded 0 phi -> rho ⊨ phi <-> sigma ⊨ phi.
proof: Proof. intros H. eapply bound_ext. apply H. lia. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullCore Undecidability(Shared.ListAutomation) Vector Lia