proposition: Lemma sat_subst {ff : falsity_flag} rho sigma phi : (forall x, eval rho (sigma x) = rho x) -> rho ⊨ phi <-> rho ⊨ (subst_form sigma phi).
proof: Proof. intros H. rewrite sat_comp. apply sat_ext. intros x. now rewrite <- H. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullCore Undecidability(Shared.ListAutomation) Vector Lia