diff --git a/tests/simple.t b/tests/simple.t
index bcda3cab5f7a83e091a1f2d79c92a2ac77558351..b608821eed730a611d876e8e6d9c027290516a8a 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -25,13 +25,12 @@ Test verify
   > theory T
   >   use TestNetwork.AsTuple
   >   use ieee_float.Float64
-  >   use real.RealInfix
   >   use caisar.NNet
   > 
   >   goal G: forall x1 x2 x3 x4 x5.
-  >      0.0 <. t'real x1 <. 0.1 ->
+  >      (0.0:t) .< x1 .< (0.5:t) ->
   >      let (y1,_,_,_,_) = nnet_apply x1 x2 x3 x4 x5 in
-  >      0.0 <. t'real y1 <. 0.1
+  >      (0.0:t) .< y1 .< (0.5:t)
   > end
   > EOF
   <autodetect>0 prover(s) added
@@ -1169,12 +1168,12 @@ Test verify
   
   function x5 [@introduced] : t19
   
-  axiom H [@introduced] : (0.0 <  tqtreal x1)
+  axiom H [@introduced] : lt 0.0 x1
   
-  axiom H1 [@introduced] : (tqtreal x1 <  0.1)
+  axiom H1 [@introduced] : lt x1 0.5
   
   goal G : match nnet_apply x1 x2 x3 x4 x5 with
-    | Tuple5 y1 _ _ _ _ -> (0.0 <  tqtreal y1) /\ (tqtreal y1 <  0.1)
+    | Tuple5 y1 _ _ _ _ -> lt 0.0 y1 /\ lt y1 0.5
     end
   
   end