proposition: Fact fol_subst_ext σ ρ A : (forall n, n ∊ fol_vars A -> σ n = ρ n) -> A⦃σ⦄ = A⦃ρ⦄.
proof: Proof. intros Hfg; revert A σ ρ Hfg. induction A as [ | p v | c A IHA B IHB | q A IHA ]; intros f g Hfg; simpl; f_equal; auto. + apply vec_map_ext; intros t Ht. apply fo_term_subst_ext; intros n Hn. apply Hfg, in_flat_map; exists t; split; auto. apply in_vec_list; auto. + apply IHA; intros n Hn; apply Hfg, in_or_app; auto. + apply IHB; intros n Hn; apply Hfg, in_or_app; auto. + apply IHA; intros [ | n ] Hn; simpl; auto; rew fot. f_equal; apply Hfg; simpl. apply in_flat_map; exists (S n); simpl; 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