proposition: Lemma ksat_ext {ff : falsity_flag} u rho xi phi : (forall x, rho x = xi x) -> rho ⊩(u,M) phi <-> xi ⊩(u,M) phi.
proof: Proof. induction phi as [ | b P v | | ] in rho, xi, u |-*; intros Hext; comp. - tauto. - erewrite Vector.map_ext. reflexivity. intros t. now apply eval_ext. - destruct b0; split; intros H v Hv Hv'; now apply (IHphi2 v rho xi Hext), (H _ Hv), (IHphi1 v rho xi Hext). - destruct q; split; intros H d; apply (IHphi _ (d .: rho) (d .: xi)). all: ((intros []; cbn; congruence) + auto). Qed.
imports: Undecidability.FOL.Semantics.Tarski.FragmentFacts Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability.FOL.Syntax.Facts Undecidability(Shared.ListAutomation)