proposition: Fact fot_def_proj n : fot_definable (fun φ => φ n).
proof: Proof. exists (£ n); intros; split; rew fot; auto; intros _ []. 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)