proposition: Lemma sat_comp {ff : falsity_flag} rho xi phi : rho ⊨ (subst_form xi phi) <-> (xi >> eval rho) ⊨ phi.
proof: Proof. induction phi as [ | b P v | | ] in rho, xi |- *; cbn. - reflexivity. - erewrite map_map, map_ext; try reflexivity. intros t. apply eval_comp. - specialize (IHphi1 rho xi). specialize (IHphi2 rho xi). destruct b0; intuition. - destruct q. + setoid_rewrite IHphi. split; intros H d; eapply sat_ext. 2, 4: apply (H d). all: intros []; cbn; trivial; now setoid_rewrite eval_comp. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Theories Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability(Shared.ListAutomation) Vector Lia