proposition: Lemma sat_single {ff : falsity_flag} (rho : nat -> D) (Phi : form) (t : term) : (eval rho t .: rho) ⊨ Phi <-> rho ⊨ subst_form (t..) Phi.
proof: Proof. rewrite sat_comp. apply sat_ext. now intros []. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullCore Undecidability(Shared.ListAutomation) Vector Lia