diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs b/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs
index 343f2f76..e78c1ed1 100644
--- a/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs
+++ b/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs
@@ -44,7 +44,7 @@ exportPropM ty =
       case (pc, ets) of
         (Cry.PFin,   [t])     -> return (Fin t)
         (Cry.PEqual, [t1,t2]) -> return (t1 :== t2)
-        (Cry.PNeq,   [t1,t2]) -> return (t1 :== t2)
+        (Cry.PNeq,   [t1,t2]) -> return (Not (t1 :== t2))
         (Cry.PGeq,   [t1,t2]) -> return (t1 :>= t2)
         _                     -> raise ()
     Cry.TCon _ _ -> raise ()