diff --git a/Language/Expression/Prop.hs b/Language/Expression/Prop.hs
--- a/Language/Expression/Prop.hs
+++ b/Language/Expression/Prop.hs
@@ -121,17 +121,17 @@
     LogNot x -> not <$> x
     LogAnd x y -> liftA2 (&&) x y
     LogOr x y -> liftA2 (||) x y
-    LogImpl x y -> liftA2 (==>) x y
-    LogEquiv x y -> liftA2 (<=>) x y
+    LogImpl x y -> liftA2 (||) (not <$> x) y
+    LogEquiv x y -> liftA2 (&&) (liftA2 (||) (not <$> x) y) (liftA2 (||) (not <$> y) x)
 
 instance HFoldableAt SBV LogicOp where
   hfoldMap = implHfoldMap $ \case
     LogLit b -> fromBool b
-    LogNot x -> bnot x
-    LogAnd x y -> x &&& y
-    LogOr x y -> x ||| y
-    LogImpl x y -> x ==> y
-    LogEquiv x y -> x <=> y
+    LogNot x -> sNot x
+    LogAnd x y -> x .&& y
+    LogOr x y -> x .|| y
+    LogImpl x y -> x .=> y
+    LogEquiv x y -> x .<=> y
 
 -- instance HEq LogicOp where
 --   liftHEq _ _ (LogLit x) (LogLit y) = x == y
diff --git a/Language/While/Syntax.hs b/Language/While/Syntax.hs
--- a/Language/While/Syntax.hs
+++ b/Language/While/Syntax.hs
@@ -79,10 +79,10 @@
     OpGT -> runcurry (.>)
     OpGE -> runcurry (.>=)
 
-    OpAnd -> runcurry (&&&)
-    OpOr -> runcurry (|||)
+    OpAnd -> runcurry (.&&)
+    OpOr -> runcurry (.||)
 
-    OpNot -> runcurry bnot
+    OpNot -> runcurry sNot
 
 -- instance EqOpMany WhileOpKind where
 --   liftEqMany (OpLit x) (OpLit y) _ = \_ _ -> x == y
diff --git a/verifiable-expressions.cabal b/verifiable-expressions.cabal
--- a/verifiable-expressions.cabal
+++ b/verifiable-expressions.cabal
@@ -1,13 +1,13 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.31.1.
+-- This file has been generated from package.yaml by hpack version 0.31.2.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: ce4006a4eb6cc4997fc47936009d3e9b564b686fb2d70bab60d3a536d8c65df7
+-- hash: ad72557a78859a1f81baf264e6f52253074bef4077f8206609ea198177c25595
 
 name:           verifiable-expressions
-version:        0.5.0
+version:        0.6.0
 synopsis:       An intermediate language for Hoare logic style verification.
 description:    A typed intermediate language for Hoare logic style verification. It defines the intermediate language and combinators to interact it.
 category:       Language
@@ -49,7 +49,7 @@
     , containers >=0.5.7 && <0.7
     , lens >=4.16.1 && <5
     , mtl >=2.0 && <3
-    , sbv >=7.0 && <8
+    , sbv >=8.0 && <9
     , transformers >=0.5 && <0.6
     , union >=0.1.1 && <0.2
     , vinyl >=0.8.1 && <0.9