proposition: Fact fol_def_fa (R : X -> (nat -> X) -> Prop) : fol_definable (fun φ => R (φ 0) (fun n => φ (S n))) -> fol_definable (fun φ => forall x, R x φ).
proof: Proof. intros (A & H1 & H2 & H3); exists (fol_quant fol_fa A); msplit 2; auto. intro; simpl; apply forall_equiv. intro; rewrite H3; simpl; tauto. 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)