proposition: Fact fol_def_vec_fa 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 φ => forall 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; auto; intros ? v; vec nil v; auto. + set (T φ := forall v x, R (x##v) φ). apply fol_def_equiv with (R := T). * intros phi; unfold T; split. - intros H v; vec split v with x; auto. - intros H ? ?; apply (H (_##_)). * unfold T; apply IHn, fol_def_fa, 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)