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