proposition: Lemma sat_ext' {ff : falsity_flag} rho xi phi : (forall x, rho x = xi x) -> rho ⊨ phi -> xi ⊨ phi.
proof: Proof. intros Hext H. rewrite sat_ext. exact H. intros x. now rewrite (Hext x). Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullCore Undecidability(Shared.ListAutomation) Vector Lia