proposition: Fact fol_subst_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 f g; auto. + f_equal. rewrite vec_map_map. apply vec_map_ext. intros A w; rew fot; auto. + f_equal; auto. + f_equal. rewrite IHA; auto. apply fol_subst_ext. intros [ | n ] _; rew fot; simpl; rew fot; simpl; auto. do 2 rewrite <- fo_term_subst_map, fo_term_subst_comp. apply fo_term_subst_ext. intros; rew fot; rewrite fo_term_subst_map; simpl; 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