proposition: Lemma ksat_comp {ff : falsity_flag} u rho xi phi : rho ⊩(u,M) phi[xi] <-> (xi >> eval rho (I := @k_interp _ M)) ⊩(u,M) phi.
proof: Proof. induction phi as [ | b P v | | ] in rho, xi, u |-*; comp. - tauto. - erewrite Vector.map_map. erewrite Vector.map_ext. 2: apply eval_comp. reflexivity. - destruct b0. setoid_rewrite IHphi1. now setoid_rewrite IHphi2. - destruct q. setoid_rewrite IHphi. split; intros H d; eapply ksat_ext. 2, 4: apply (H d). all: intros []; cbn; trivial; unfold funcomp; now erewrite eval_comp. Qed.
imports: Undecidability.FOL.Semantics.Tarski.FragmentFacts Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability.FOL.Syntax.Facts Undecidability(Shared.ListAutomation)