proposition: Fact fo_term_syms_subst P f t : (forall n, In n (fo_term_vars t) -> Forall P (fo_term_syms (f n))) -> Forall P (fo_term_syms t) -> Forall P (fo_term_syms (t⟬f⟭)).
proof: Proof. induction t as [ n | s v IH ]; intros H1 H2; rew fot. + apply H1; simpl; auto. + constructor. * rewrite Forall_forall in H2; apply H2; rew fot; left; auto. * rewrite Forall_forall; intros x; rewrite in_flat_map. intros (s' & H3 & H4). rewrite vec_list_vec_map, in_map_iff in H3. destruct H3 as (t & <- & H3). apply vec_list_inv in H3. destruct H3 as (p & ->). revert x H4; apply Forall_forall, IH; auto. - intros; apply H1; rew fot; apply in_flat_map. exists (vec_pos v p); split; auto. apply in_vec_list, in_vec_pos. - revert H2; do 2 rewrite Forall_forall. intros H2 x Hx; apply H2; rew fot. right; apply in_flat_map. exists (vec_pos v p); split; auto. apply in_vec_list, in_vec_pos. Qed.
imports: List Arith Lia Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils decidable fol_ops fo_sig)