diff --git a/proof-libs/fstar/core/Core.Core_arch.X86.fsti b/proof-libs/fstar/core/Core.Core_arch.X86.fsti
new file mode 100644
index 000000000..4d115808c
--- /dev/null
+++ b/proof-libs/fstar/core/Core.Core_arch.X86.fsti
@@ -0,0 +1,3 @@
+module Core.Core_arch.X86
+
+val t____m256i:Type
diff --git a/proof-libs/fstar/core/Core.Core_arch.fsti b/proof-libs/fstar/core/Core.Core_arch.fsti
new file mode 100644
index 000000000..a3921ebe3
--- /dev/null
+++ b/proof-libs/fstar/core/Core.Core_arch.fsti
@@ -0,0 +1,2 @@
+module Core.Core_arch
+