proposition: Theorem fol_sem_subst φ σ A : ⟪ A⦃σ⦄ ⟫ φ <-> ⟪A⟫ (fun n => ⟦σ n⟧ φ).
proof: Proof. revert φ σ; induction A as [ | p v | b A IHA B IHB | q A IHA ]; simpl; intros phi f; try tauto. + fol equiv rel. rewrite vec_map_map; apply vec_map_ext. intros; rewrite fo_term_sem_subst; auto. + apply fol_bin_sem_ext; auto. + apply fol_quant_sem_ext. intros x; rewrite IHA. apply fol_sem_ext. intros [ | n ] _; simpl; rew fot; simpl; auto. rewrite <- fo_term_subst_map; rew fot. apply fo_term_sem_ext; intros; rew fot; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms) Undecidability.Shared.ListAutomation