proposition: Fact fol_syms_subst P σ (A : 𝔽) : (forall n, n ∊ fol_vars A -> Forall P (fo_term_syms (σ n))) -> Forall P (fol_syms A) -> Forall P (fol_syms (A⦃σ⦄)).
proof: Proof. revert σ. induction A as [ | s r | b A HA B HB | q A HA ]; intros f Hf H; simpl; auto. + rewrite Forall_forall in H |- *. intros s'; rewrite in_flat_map. intros (t & Ht); revert Ht. rewrite vec_list_vec_map, in_map_iff. intros ((t' & <- & H1) & H2). revert s' H2; apply Forall_forall. apply fo_term_syms_subst. simpl in H, Hf. * intros n Hn; apply Hf, in_flat_map. exists t'; auto. * apply Forall_forall; intros s' Hs'. apply H, in_flat_map; exists t'; auto. + simpl in H; rewrite Forall_app in H. rewrite Forall_app; split. * apply HA; try tauto. intros; apply Hf, in_or_app; auto. * apply HB; try tauto. intros; apply Hf, in_or_app; auto. + simpl in H; apply HA; auto. intros [ | n ]; simpl; rew fot; auto. rewrite fo_term_syms_map; intros Hn. apply Hf, 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