proposition: Fact fol_def_vec_ex n (R : vec X n -> (nat -> X) -> Prop) : (fol_definable ls lr M (fun φ => R (env_vec φ n) (env_env φ n))) -> fol_definable ls lr M (fun φ => exists v, R v φ).
proof: Proof. revert R; induction n as [ | n IHn ]; intros R HR. + revert HR; apply fol_def_equiv; intros phi; simpl. split. * exists vec_nil; auto. * intros (v & Hv); revert Hv; vec nil v; auto. + set (T φ := exists v x, R (x##v) φ). apply fol_def_equiv with (R := T). * intros phi; unfold T; split. - intros (v & x & Hv); exists (x##v); auto. - intros (v & Hv); revert Hv; vec split v with x; exists v, x; auto. * unfold T; apply IHn, fol_def_ex, HR. 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)