diff --git a/share/libc/__fc_define_fd_set_t.h b/share/libc/__fc_define_fd_set_t.h
index 5f9b7c721b2124a2158961a07c7db38eda5506e3..5e6bbe0272593c03712707a3966a0cd086f32250 100644
--- a/share/libc/__fc_define_fd_set_t.h
+++ b/share/libc/__fc_define_fd_set_t.h
@@ -29,40 +29,6 @@ __PUSH_FC_STDLIB
 __BEGIN_DECLS
 typedef struct __fc_fd_set { long __fc_fd_set[FD_SETSIZE / NFDBITS]; } fd_set;
 
-/*@
-  requires valid_fdset: \valid(fdset);
-  requires initialization: \initialized(fdset);
-  assigns *fdset \from *fdset, indirect:fd;
-*/
-extern void FD_CLR(int fd, fd_set *fdset);
-#define FD_CLR FD_CLR
-
-// Note: the 2nd argument in FD_ISSET is not const in some implementations
-// due to historical and compatibility reasons.
-/*@
-  requires valid_fdset: \valid_read(fdset);
-  requires initialization: \initialized(fdset);
-  assigns \result \from indirect:*fdset, indirect:fd;
-*/
-extern int FD_ISSET(int fd, const fd_set *fdset);
-#define FD_ISSET FD_ISSET
-
-/*@
-  requires valid_fdset: \valid(fdset);
-  requires initialization: \initialized(fdset);
-  assigns *fdset \from *fdset, indirect:fd;
-*/
-extern void FD_SET(int fd, fd_set *fdset);
-#define FD_SET FD_SET
-
-/*@
-  requires valid_fdset: \valid(fdset);
-  assigns *fdset \from \nothing;
-  ensures initialization: \initialized(fdset);
-*/
-extern void FD_ZERO(fd_set *fdset);
-#define FD_ZERO FD_ZERO
-
 __END_DECLS
 __POP_FC_STDLIB
 #endif
diff --git a/share/libc/sys/select.h b/share/libc/sys/select.h
index c680c04d2e2ec48a879ee4b74dccc8468abfbdd2..d3ceb4b58487f35543d5c5fdf13ec56deea00c6a 100644
--- a/share/libc/sys/select.h
+++ b/share/libc/sys/select.h
@@ -28,6 +28,40 @@ __BEGIN_DECLS
 
 #include "../__fc_select.h"
 
+/*@
+  requires valid_fdset: \valid(fdset);
+  requires initialization: \initialized(fdset);
+  assigns *fdset \from *fdset, indirect:fd;
+*/
+extern void FD_CLR(int fd, fd_set *fdset);
+#define FD_CLR FD_CLR
+
+// Note: the 2nd argument in FD_ISSET is not const in some implementations
+// due to historical and compatibility reasons.
+/*@
+  requires valid_fdset: \valid_read(fdset);
+  requires initialization: \initialized(fdset);
+  assigns \result \from indirect:*fdset, indirect:fd;
+*/
+extern int FD_ISSET(int fd, const fd_set *fdset);
+#define FD_ISSET FD_ISSET
+
+/*@
+  requires valid_fdset: \valid(fdset);
+  requires initialization: \initialized(fdset);
+  assigns *fdset \from *fdset, indirect:fd;
+*/
+extern void FD_SET(int fd, fd_set *fdset);
+#define FD_SET FD_SET
+
+/*@
+  requires valid_fdset: \valid(fdset);
+  assigns *fdset \from \nothing;
+  ensures initialization: \initialized(fdset);
+*/
+extern void FD_ZERO(fd_set *fdset);
+#define FD_ZERO FD_ZERO
+
 __END_DECLS
 __POP_FC_STDLIB
 #endif