proposition: Lemma sat_atom_subst_compat rho phi n : sat rho (phi [s/atom]) <-> @sat _ _ _ (interp_s (rho n)) _ rho phi.
proof: Proof. Proof using Hresp. unfold interp_s, lift_s_semantically. revert rho n. induction phi as [|t1 t2|ff [] phi IHphi psi IHpsi|ff [] phi IHphi]; split. - intros H; apply H. - intros H; apply H. - cbn; intros H. eapply sat_ext with (((rho_from_vec t $n) >> eval rho)). 1: intros x; unfold funcomp. now apply rho_from_vec_map. rewrite <- sat_comp. rewrite Hresp. now rewrite semantic_lifting_correct. - cbn; intros H. eapply (@sat_ext _ _ _ _ _ (((rho_from_vec t $n) >> eval rho))) in H. 2: intros x; unfold funcomp; symmetry; now apply rho_from_vec_map. rewrite <- sat_comp in H. rewrite Hresp in H. now rewrite semantic_lifting_correct in H. - cbn; intros H1 Hphi. apply IHpsi. 1:easy. apply H1. apply IHphi with n. 1:easy. apply Hphi. - cbn; intros H1 Hphi. apply IHpsi with n. 1:easy. apply H1, IHphi. 1:easy. apply Hphi. - cbn; intros H1 d. apply (IHphi s Hresp (d.:rho) (S n)). apply H1. - cbn; intros H1 d. apply (IHphi s Hresp (d.:rho) (S n)). apply H1. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Theories Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability(Shared.ListAutomation) Vector Lia