proposition: Fact fol_def_subst (R : (nat -> X) -> Prop) (f : nat -> (nat -> X) -> X) : (forall n, fot_definable (f n)) -> fol_definable R -> fol_definable (fun φ => R (fun n => f n φ)).
proof: Proof. intros H1 H2. generalize (fol_def_ext H2); intros H3. destruct H2 as (A & G1 & G2 & HA). set (rho := fun n => proj1_sig (H1 n)). exists (fol_subst rho A); msplit 2. + red; apply Forall_forall; apply fol_syms_subst. * intros n Hn; rewrite Forall_forall. intro; apply (fun n => proj2_sig (H1 n)). * apply Forall_forall, G1. + rewrite fol_rels_subst; auto. + intros phi. rewrite fol_sem_subst, HA. apply H3; intro; unfold rho; rew fot. apply (fun n => proj2_sig (H1 n)). Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic)