diff --git a/symbolic-apps/src/ZkFold/Symbolic/Apps/KYC.hs b/symbolic-apps/src/ZkFold/Symbolic/Apps/KYC.hs
index 61920a3df..c6b3c1ada 100644
--- a/symbolic-apps/src/ZkFold/Symbolic/Apps/KYC.hs
+++ b/symbolic-apps/src/ZkFold/Symbolic/Apps/KYC.hs
@@ -61,7 +61,7 @@ kycExample :: forall n r rsc context . (
   Symbolic context
   , KnownNat n
   , KnownNat rsc
-  , Eq (Bool context) (KYCHash context)
+  , Eq (KYCHash context)
   , KnownRegisterSize r
   , KnownRegisters context 64 r
   , KnownNat (Ceil (GetRegisterSize (BaseField context) 64 r) OrdWord)
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs
index 551189976..7f91eeabb 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs
@@ -62,22 +62,23 @@ type Fq12 = Ext2 Fq6 IP3
 instance Field field => WeierstrassCurve "BLS12-381" field where
   weierstrassB = fromConstant (4 :: Natural)
 
-type BLS12_381_Point baseField = Weierstrass "BLS12-381" (Point Bool baseField)
+type BLS12_381_Point baseField = Weierstrass "BLS12-381" (Point baseField)
 
 type BLS12_381_CompressedPoint baseField =
-  Weierstrass "BLS12-381" (CompressedPoint Bool baseField)
+  Weierstrass "BLS12-381" (CompressedPoint baseField)
 
 instance
-  ( Symbolic.Conditional Bool field
-  , Symbolic.Eq Bool field
+  ( Symbolic.Conditional (Symbolic.BooleanOf field) field
+  , Symbolic.Eq field
   , FiniteField field
   , Ord field
-  ) => Compressible Bool (BLS12_381_Point field) where
+  , Symbolic.BooleanOf field ~ Bool
+  ) => Compressible (BLS12_381_Point field) where
     type Compressed (BLS12_381_Point field) = BLS12_381_CompressedPoint field
     pointCompressed x yBit = Weierstrass (CompressedPoint x yBit False)
     compress (Weierstrass (Point x y isInf)) =
       if isInf then pointInf
-      else pointCompressed @Bool @(BLS12_381_Point field) x (y > negate y)
+      else pointCompressed @(BLS12_381_Point field) x (y > negate y)
     decompress (Weierstrass (CompressedPoint x bigY isInf)) =
       if isInf then pointInf else
         let b = weierstrassB @"BLS12-381"
@@ -164,8 +165,8 @@ instance Binary BLS12_381_G1_Point where
             let x = ofBytes (byteXhead:bytesXtail)
                 bigY = testBit byte 2
             if compressed then return $
-              decompress @Bool @BLS12_381_G1_Point
-                (pointCompressed @Bool @BLS12_381_G1_Point x bigY)
+              decompress @BLS12_381_G1_Point
+                (pointCompressed @BLS12_381_G1_Point x bigY)
             else do
                 bytesY <- replicateM 48 getWord8
                 let y = ofBytes bytesY
@@ -190,7 +191,7 @@ instance Binary BLS12_381_G1_CompressedPoint where
             bytesXtail <- replicateM 47 getWord8
             let x = ofBytes (byteXhead:bytesXtail)
                 bigY = testBit byte 2
-            pointCompressed @Bool @BLS12_381_G1_Point x <$>
+            pointCompressed @BLS12_381_G1_Point x <$>
               if compressed then return bigY else do
                 bytesY <- replicateM 48 getWord8
                 let y :: Fq = ofBytes bytesY
@@ -222,8 +223,8 @@ instance Binary BLS12_381_G2_Point where
                 x0 = ofBytes bytesX0
                 bigY = testBit byte 2
             if compressed then return $
-              decompress @Bool @BLS12_381_G2_Point
-                (pointCompressed @Bool @BLS12_381_G2_Point (Ext2 x0 x1) bigY)
+              decompress @BLS12_381_G2_Point
+                (pointCompressed @BLS12_381_G2_Point (Ext2 x0 x1) bigY)
             else do
                 bytesY1 <- replicateM 48 getWord8
                 bytesY0 <- replicateM 48 getWord8
@@ -254,7 +255,7 @@ instance Binary BLS12_381_G2_CompressedPoint where
                 x0 = ofBytes bytesX0
                 x = Ext2 x0 x1
                 bigY = testBit byte 2
-            pointCompressed @Bool @BLS12_381_G2_Point x <$>
+            pointCompressed @BLS12_381_G2_Point x <$>
               if compressed then return bigY else do
                 bytesY1 <- replicateM 48 getWord8
                 bytesY0 <- replicateM 48 getWord8
@@ -269,7 +270,14 @@ instance Binary BLS12_381_G2_CompressedPoint where
 -- | An image of a pairing is a cyclic multiplicative subgroup of @'Fq12'@
 -- of order @'BLS12_381_Scalar'@.
 newtype BLS12_381_GT = BLS12_381_GT Fq12
-    deriving newtype (Eq, Show, MultiplicativeSemigroup, MultiplicativeMonoid, Symbolic.Eq Bool)
+    deriving newtype
+        ( Eq
+        , Show
+        , MultiplicativeSemigroup
+        , MultiplicativeMonoid
+        , Symbolic.Conditional Prelude.Bool
+        , Symbolic.Eq
+        )
 
 instance Exponent BLS12_381_GT Natural where
     BLS12_381_GT a ^ p = BLS12_381_GT (a ^ p)
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BN254.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BN254.hs
index e94facb7e..4347d6f0f 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BN254.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BN254.hs
@@ -31,6 +31,7 @@ import           ZkFold.Base.Algebra.Basic.Number
 import           ZkFold.Base.Algebra.EllipticCurve.Class
 import           ZkFold.Base.Algebra.EllipticCurve.Pairing
 import           ZkFold.Base.Algebra.Polynomials.Univariate (toPoly)
+import           ZkFold.Symbolic.Data.Conditional
 import           ZkFold.Symbolic.Data.Eq
 
 -------------------------- Scalar field & field towers -------------------------
@@ -70,7 +71,7 @@ type Fp12 = Ext2 Fp6 "IP3"
 
 type BN254_G1_Point = BN254_G1_PointOf Fp
 
-type BN254_G1_PointOf field = Weierstrass "BN254_G1" (Point Bool field)
+type BN254_G1_PointOf field = Weierstrass "BN254_G1" (Point field)
 
 instance Field field => WeierstrassCurve "BN254_G1" field where
   weierstrassB = fromConstant (3 :: Natural)
@@ -86,7 +87,7 @@ instance Scale Fr BN254_G1_Point where
 
 type BN254_G2_Point = BN254_G2_PointOf Fp2
 
-type BN254_G2_PointOf field = Weierstrass "BN254_G2" (Point Bool field)
+type BN254_G2_PointOf field = Weierstrass "BN254_G2" (Point field)
 
 instance WeierstrassCurve "BN254_G2" Fp2 where
   weierstrassB =
@@ -107,7 +108,14 @@ instance Scale Fr BN254_G2_Point where
 ------------------------------- Pairing ----------------------------------------
 
 newtype BN254_GT = BN254_GT Fp12
-  deriving (Prelude.Eq, Show, MultiplicativeSemigroup, MultiplicativeMonoid, Eq Prelude.Bool)
+  deriving
+    ( Prelude.Eq
+    , Show
+    , MultiplicativeSemigroup
+    , MultiplicativeMonoid
+    , Conditional Prelude.Bool
+    , Eq
+    )
 
 instance Exponent BN254_GT Natural where
   BN254_GT e ^ p = BN254_GT (e ^ p)
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
index 5c7d5b1c3..dff981e42 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
@@ -56,15 +56,15 @@ The geometric group law of the elliptic curve is:
 -}
 class
   ( Field (BaseFieldOf point)
-  , Eq bool (BaseFieldOf point)
+  , Eq (BaseFieldOf point)
   , Planar (BaseFieldOf point) point
   , AdditiveGroup point
-  ) => EllipticCurve bool point where
+  ) => EllipticCurve point where
     type CurveOf point :: Symbol
     type BaseFieldOf point :: Type
     -- | `isOnCurve` validates an equation for a plane algebraic curve
     -- which has degree 3 up to some birational equivalence.
-    isOnCurve :: point -> bool
+    isOnCurve :: point -> BooleanOf (BaseFieldOf point)
 
 {- | Both the ECDSA and ECDH algorithms make use of
 the elliptic curve discrete logarithm problem, ECDLP.
@@ -116,9 +116,12 @@ class Field field => TwistedEdwardsCurve (curve :: Symbol) field where
   twistedEdwardsA :: field
   twistedEdwardsD :: field
 
-class Compressible bool point where
+class Eq (BaseFieldOf point) => Compressible point where
   type Compressed point :: Type
-  pointCompressed :: BaseFieldOf point -> bool -> Compressed point
+  pointCompressed
+    :: BaseFieldOf point
+    -> BooleanOf (BaseFieldOf point)
+    -> Compressed point
   compress :: point -> Compressed point
   decompress :: Compressed point -> point
 
@@ -149,66 +152,62 @@ deriving newtype instance Prelude.Eq point
 deriving newtype instance Prelude.Show point
   => Prelude.Show (Weierstrass curve point)
 instance
-  ( Arbitrary (ScalarFieldOf (Weierstrass curve (Point Prelude.Bool field)))
-  , CyclicGroup (Weierstrass curve (Point Prelude.Bool field))
-  ) => Arbitrary (Weierstrass curve (Point Prelude.Bool field)) where
+  ( Arbitrary (ScalarFieldOf (Weierstrass curve (Point field)))
+  , CyclicGroup (Weierstrass curve (Point field))
+  ) => Arbitrary (Weierstrass curve (Point field)) where
     arbitrary = do
-      c <- arbitrary @(ScalarFieldOf (Weierstrass curve (Point Prelude.Bool field)))
+      c <- arbitrary @(ScalarFieldOf (Weierstrass curve (Point field)))
       return $ scale c pointGen
 instance
-  ( Arbitrary (ScalarFieldOf (Weierstrass curve (Point Prelude.Bool field)))
-  , CyclicGroup (Weierstrass curve (Point Prelude.Bool field))
-  , Compressible Prelude.Bool (Weierstrass curve (Point Prelude.Bool field))
-  , Compressed (Weierstrass curve (Point Prelude.Bool field)) ~ Weierstrass curve (CompressedPoint Prelude.Bool field)
-  ) => Arbitrary (Weierstrass curve (CompressedPoint Prelude.Bool field)) where
+  ( Arbitrary (ScalarFieldOf (Weierstrass curve (Point field)))
+  , CyclicGroup (Weierstrass curve (Point field))
+  , Compressible (Weierstrass curve (Point field))
+  , Compressed (Weierstrass curve (Point field))
+    ~ Weierstrass curve (CompressedPoint field)
+  ) => Arbitrary (Weierstrass curve (CompressedPoint field)) where
     arbitrary = do
-      c <- arbitrary @(ScalarFieldOf (Weierstrass curve (Point Prelude.Bool field)))
-      return $ compress @Prelude.Bool (scale c (pointGen @(Weierstrass curve (Point Prelude.Bool field))))
+      c <- arbitrary @(Weierstrass curve (Point field))
+      return $ compress c
 instance
   ( WeierstrassCurve curve field
-  , Conditional bool bool
-  , Conditional bool field
-  , Eq bool field
+  , Conditional (BooleanOf field) (BooleanOf field)
+  , Conditional (BooleanOf field) field
+  , Eq field
   , Field field
-  ) => EllipticCurve bool (Weierstrass curve (Point bool field)) where
-    type CurveOf (Weierstrass curve (Point bool field)) = curve
-    type BaseFieldOf (Weierstrass curve (Point bool field)) = field
+  ) => EllipticCurve (Weierstrass curve (Point field)) where
+    type CurveOf (Weierstrass curve (Point field)) = curve
+    type BaseFieldOf (Weierstrass curve (Point field)) = field
     isOnCurve (Weierstrass (Point x y isInf)) =
       if isInf then x == zero else
       let b = weierstrassB @curve in y*y == x*x*x + b
 deriving newtype instance
-  ( SymbolicOutput bool
-  , SymbolicOutput field
-  , Context field ~ Context bool
-  ) => SymbolicData (Weierstrass curve (Point bool field))
+  ( SymbolicEq field
+  ) => SymbolicData (Weierstrass curve (Point field))
 instance
-  ( SymbolicInput field
-  , Context field ~ ctx
-  , Symbolic ctx
-  , WeierstrassCurve curve field
-  , Eq (Bool ctx) field
-  , Conditional (Bool ctx) field
-  ) => SymbolicInput (Weierstrass curve (Point (Bool ctx) field)) where
+  ( WeierstrassCurve curve field
+  , SymbolicEq field
+  , SymbolicInput field
+  ) => SymbolicInput (Weierstrass curve (Point field)) where
     isValid = isOnCurve
 deriving newtype instance Conditional bool point
   => Conditional bool (Weierstrass curve point)
-deriving newtype instance Eq bool point
-  => Eq bool (Weierstrass curve point)
+deriving newtype instance Eq point
+  => Eq (Weierstrass curve point)
 deriving newtype instance HasPointInf point
   => HasPointInf (Weierstrass curve point)
 deriving newtype instance Planar field point
   => Planar field (Weierstrass curve point)
 instance
   ( WeierstrassCurve curve field
-  , Conditional bool bool
-  , Conditional bool field
-  , Eq bool field
+  , Conditional (BooleanOf field) (BooleanOf field)
+  , Conditional (BooleanOf field) field
+  , Eq field
   , Field field
-  ) => AdditiveSemigroup (Weierstrass curve (Point bool field)) where
+  ) => AdditiveSemigroup (Weierstrass curve (Point field)) where
     pt0@(Weierstrass (Point x0 y0 isInf0)) + pt1@(Weierstrass (Point x1 y1 isInf1)) =
       if isInf0 then pt1 else if isInf1 then pt0 -- additive identity
-      else if x0 == x1 && y0 + y1 == zero :: bool then pointInf -- additive inverse
-      else let slope = if x0 == x1 && y0 == y1 :: bool
+      else if x0 == x1 && y0 + y1 == zero then pointInf -- additive inverse
+      else let slope = if x0 == x1 && y0 == y1
                        then (x0 * x0 + x0 * x0 + x0 * x0) // (y0 + y0) -- tangent
                        else (y1 - y0) // (x1 - x0) -- secant
                x2 = slope * slope - x0 - x1
@@ -216,36 +215,36 @@ instance
             in pointXY x2 y2
 instance
   ( WeierstrassCurve curve field
-  , Conditional bool bool
-  , Conditional bool field
-  , Eq bool field
+  , Conditional (BooleanOf field) (BooleanOf field)
+  , Conditional (BooleanOf field) field
+  , Eq field
   , Field field
-  ) => AdditiveMonoid (Weierstrass curve (Point bool field)) where
+  ) => AdditiveMonoid (Weierstrass curve (Point field)) where
     zero = pointInf
 instance
   ( WeierstrassCurve curve field
-  , Conditional bool bool
-  , Conditional bool field
-  , Eq bool field
+  , Conditional (BooleanOf field) (BooleanOf field)
+  , Conditional (BooleanOf field) field
+  , Eq field
   , Field field
-  ) => AdditiveGroup (Weierstrass curve (Point bool field)) where
+  ) => AdditiveGroup (Weierstrass curve (Point field)) where
     negate pt@(Weierstrass (Point x y isInf)) =
       if isInf then pt else pointXY x (negate y)
 instance
   ( WeierstrassCurve curve field
-  , Conditional bool bool
-  , Conditional bool field
-  , Eq bool field
+  , Conditional (BooleanOf field) (BooleanOf field)
+  , Conditional (BooleanOf field) field
+  , Eq field
   , Field field
-  ) => Scale Natural (Weierstrass curve (Point bool field)) where
+  ) => Scale Natural (Weierstrass curve (Point field)) where
   scale = natScale
 instance
   ( WeierstrassCurve curve field
-  , Conditional bool bool
-  , Conditional bool field
-  , Eq bool field
+  , Conditional (BooleanOf field) (BooleanOf field)
+  , Conditional (BooleanOf field) field
+  , Eq field
   , Field field
-  ) => Scale Integer (Weierstrass curve (Point bool field)) where
+  ) => Scale Integer (Weierstrass curve (Point field)) where
   scale = intScale
 
 {- | `TwistedEdwards` tags a `Planar` @point@, over a `Field` @field@,
@@ -254,8 +253,8 @@ newtype TwistedEdwards curve point = TwistedEdwards {pointTwistedEdwards :: poin
 instance
   ( TwistedEdwardsCurve curve field
   , Field field
-  , Eq bool field
-  ) => EllipticCurve bool (TwistedEdwards curve (AffinePoint field)) where
+  , Eq field
+  ) => EllipticCurve (TwistedEdwards curve (AffinePoint field)) where
     type CurveOf (TwistedEdwards curve (AffinePoint field)) = curve
     type BaseFieldOf (TwistedEdwards curve (AffinePoint field)) = field
     isOnCurve (TwistedEdwards (AffinePoint x y)) =
@@ -269,14 +268,13 @@ instance
   , Context field ~ ctx
   , Symbolic ctx
   , TwistedEdwardsCurve curve field
-  , Eq (Bool ctx) field
-  , Conditional (Bool ctx) field
+  , SymbolicEq field
   ) => SymbolicInput (TwistedEdwards curve (AffinePoint field)) where
     isValid = isOnCurve
 deriving newtype instance Conditional bool point
   => Conditional bool (TwistedEdwards curve point)
-deriving newtype instance Eq bool point
-  => Eq bool (TwistedEdwards curve point)
+deriving newtype instance Eq point
+  => Eq (TwistedEdwards curve point)
 deriving newtype instance HasPointInf point
   => HasPointInf (TwistedEdwards curve point)
 deriving newtype instance Planar field point
@@ -313,52 +311,60 @@ instance
   scale = intScale
 
 {- | A type of points in the projective plane. -}
-data Point bool field = Point
+data Point field = Point
   { _x    :: field
   , _y    :: field
-  , _zBit :: bool
-  } deriving (Generic, Prelude.Eq)
+  , _zBit :: BooleanOf field
+  } deriving (Generic)
+deriving instance (Prelude.Eq (BooleanOf field), Prelude.Eq field)
+  => Prelude.Eq (Point field)
 instance
-  ( SymbolicOutput bool
+  ( SymbolicOutput (BooleanOf field)
   , SymbolicOutput field
-  , Context field ~ Context bool
-  ) => SymbolicData (Point bool field)
-instance BoolType bool => Planar field (Point bool field) where
+  , Context field ~ Context (BooleanOf field)
+  ) => SymbolicData (Point field)
+instance Eq field => Planar field (Point field) where
   pointXY x y = Point x y false
-instance (BoolType bool, Semiring field) => HasPointInf (Point bool field) where
+instance (Semiring field, Eq field) => HasPointInf (Point field) where
   pointInf = Point zero one true
-instance Prelude.Show field => Prelude.Show (Point Prelude.Bool field) where
+instance (Prelude.Show field, BooleanOf field ~ Prelude.Bool)
+  => Prelude.Show (Point field) where
   show (Point x y isInf) =
     if isInf then "pointInf" else Prelude.mconcat
       ["(", Prelude.show x, ", ", Prelude.show y, ")"]
 instance
   ( Conditional bool bool
   , Conditional bool field
-  ) => Conditional bool (Point bool field)
+  , bool ~ BooleanOf field
+  ) => Conditional bool (Point field)
 instance
-  ( Conditional bool bool
-  , Eq bool bool
-  , Eq bool field
+  ( BooleanOf (BooleanOf field) ~ BooleanOf field
+  , Eq (BooleanOf field)
+  , Eq field
   , Field field
-  ) => Eq bool (Point bool field) where
+  ) => Eq (Point field) where
     Point x0 y0 isInf0 == Point x1 y1 isInf1 =
       if not isInf0 && not isInf1
       then x0 == x1 && y0 == y1
       else isInf0 && isInf1 && x1*y0 == x0*y1 -- same slope y0//x0 = y1//x1
     pt0 /= pt1 = not (pt0 == pt1)
 
-data CompressedPoint bool field = CompressedPoint
+data CompressedPoint field = CompressedPoint
   { _x    :: field
-  , _yBit :: bool
-  , _zBit :: bool
-  } deriving (Generic, Prelude.Show, Prelude.Eq)
+  , _yBit :: BooleanOf field
+  , _zBit :: BooleanOf field
+  } deriving Generic
+deriving instance (Prelude.Show (BooleanOf field), Prelude.Show field)
+  => Prelude.Show (CompressedPoint field)
+deriving instance (Prelude.Eq (BooleanOf field), Prelude.Eq field)
+  => Prelude.Eq (CompressedPoint field)
 instance
-  ( SymbolicOutput bool
+  ( SymbolicOutput (BooleanOf field)
   , SymbolicOutput field
-  , Context field ~ Context bool
-  ) => SymbolicData (CompressedPoint bool field)
-instance (BoolType bool, AdditiveMonoid field)
-  => HasPointInf (CompressedPoint bool field) where
+  , Context field ~ Context (BooleanOf field)
+  ) => SymbolicData (CompressedPoint field)
+instance (BoolType (BooleanOf field), AdditiveMonoid field)
+  => HasPointInf (CompressedPoint field) where
     pointInf = CompressedPoint zero true true
 
 data AffinePoint field = AffinePoint
@@ -369,7 +375,6 @@ instance SymbolicOutput field => SymbolicData (AffinePoint field)
 instance Planar field (AffinePoint field) where pointXY = AffinePoint
 instance Conditional bool field => Conditional bool (AffinePoint field)
 instance
-  ( BoolType bool
-  , Eq bool field
+  ( Eq field
   , Field field
-  ) => Eq bool (AffinePoint field)
+  ) => Eq (AffinePoint field)
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pairing.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pairing.hs
index 358644466..c6b353a95 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pairing.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pairing.hs
@@ -40,36 +40,36 @@ finalExponentiation x = x ^ ((p ^ (12 :: Natural) -! 1) `div` r)
     p = order @baseField
     r = order @scalarField
 
-millerAlgorithmBLS12 ::forall c d bool fldC fldD i j g.
+millerAlgorithmBLS12 ::forall c d fldC fldD i j g.
   WeierstrassCurve d fldD =>
-  Eq bool fldD =>
+  Eq fldD =>
   FiniteField fldC =>
   Scale fldC fldD =>
-  Conditional bool bool =>
-  Conditional bool fldD =>
+  Conditional (BooleanOf fldD) (BooleanOf fldD) =>
+  BooleanOf fldC ~ BooleanOf fldD =>
   Untwisted fldD i j ~ g =>
   Field g =>
   [Int8] ->
-  Weierstrass c (Point bool fldC) ->
-  Weierstrass d (Point bool fldD) ->
+  Weierstrass c (Point fldC) ->
+  Weierstrass d (Point fldD) ->
   g
 millerAlgorithmBLS12 (x:xs) p q = snd $
   millerLoop p q xs (H.bool (negate q) q (x Prelude.> 0), one)
 millerAlgorithmBLS12 _ _ _ = one
 
-millerAlgorithmBN :: forall c d bool fldC fldD i j g.
+millerAlgorithmBN :: forall c d fldC fldD i j g.
   WeierstrassCurve d fldD =>
-  Eq bool fldD =>
+  Eq fldD =>
   FiniteField fldC =>
   Scale fldC fldD =>
-  Conditional bool bool =>
-  Conditional bool fldD =>
+  Conditional (BooleanOf fldD) (BooleanOf fldD) =>
+  BooleanOf fldC ~ BooleanOf fldD =>
   Untwisted fldD i j ~ g =>
   Field g =>
   fldD ->
   [Int8] ->
-  Weierstrass c (Point bool fldC) ->
-  Weierstrass d (Point bool fldD) ->
+  Weierstrass c (Point fldC) ->
+  Weierstrass d (Point fldD) ->
   g
 millerAlgorithmBN xi (x:xs) p q = finalStepBN xi p q $
   millerLoop p q xs (H.bool (negate q) q (x Prelude.> 0), one)
@@ -77,19 +77,19 @@ millerAlgorithmBN _ _ _ _ = one
 
 -- --------------------------------------------------------------------------------
 
-finalStepBN :: forall c d bool fldC fldD i j g.
+finalStepBN :: forall c d fldC fldD i j g.
   WeierstrassCurve d fldD =>
-  Eq bool fldD =>
+  Eq fldD =>
   FiniteField fldC =>
   Scale fldC fldD =>
-  Conditional bool bool =>
-  Conditional bool fldD =>
+  Conditional (BooleanOf fldD) (BooleanOf fldD) =>
+  BooleanOf fldC ~ BooleanOf fldD =>
   Untwisted fldD i j ~ g =>
   Field g =>
   fldD ->
-  Weierstrass c (Point bool fldC) ->
-  Weierstrass d (Point bool fldD) ->
-  (Weierstrass d (Point bool fldD), g) ->
+  Weierstrass c (Point fldC) ->
+  Weierstrass d (Point fldD) ->
+  (Weierstrass d (Point fldD), g) ->
   g
 finalStepBN xi p q (t, f) = f * f' * f''
   where
@@ -101,18 +101,18 @@ finalStepBN xi p q (t, f) = f * f' * f''
 
 millerLoop ::
   WeierstrassCurve d fldD =>
-  Eq bool fldD =>
+  Eq fldD =>
   Field fldC =>
   Scale fldC fldD =>
-  Conditional bool bool =>
-  Conditional bool fldD =>
+  Conditional (BooleanOf fldD) (BooleanOf fldD) =>
+  BooleanOf fldC ~ BooleanOf fldD =>
   Untwisted fldD i j ~ g =>
   Field g =>
-  Weierstrass c (Point bool fldC) ->
-  Weierstrass d (Point bool fldD) ->
+  Weierstrass c (Point fldC) ->
+  Weierstrass d (Point fldD) ->
   [Int8] ->
-  (Weierstrass d (Point bool fldD), g) ->
-  (Weierstrass d (Point bool fldD), g)
+  (Weierstrass d (Point fldD), g) ->
+  (Weierstrass d (Point fldD), g)
 millerLoop p q = impl
   where impl []     tf = tf
         impl (x:xs) tf
@@ -124,10 +124,11 @@ millerLoop p q = impl
 --------------------------------------------------------------------------------
 
 frobTwisted ::
-  forall c bool fld.
+  forall c fld.
   ( WeierstrassCurve c fld
-  , Conditional bool bool, Conditional bool fld
-  ) => Natural -> fld -> Weierstrass c (Point bool fld) -> Weierstrass c (Point bool fld)
+  , Conditional (BooleanOf fld) (BooleanOf fld)
+  , Eq fld
+  ) => Natural -> fld -> Weierstrass c (Point fld) -> Weierstrass c (Point fld)
 frobTwisted q xi (Weierstrass (Point x y isInf)) =
   if isInf then pointInf else pointXY ((x ^ q) * (xi ^ tx)) ((y ^ q) * (xi ^ ty))
   where
@@ -136,53 +137,55 @@ frobTwisted q xi (Weierstrass (Point x y isInf)) =
 
 additionStep ::
   WeierstrassCurve d fldD =>
-  Eq bool fldD =>
+  Eq fldD =>
   Field fldC =>
   Scale fldC fldD =>
-  Conditional bool bool =>
-  Conditional bool fldD =>
+  BooleanOf fldC ~ BooleanOf fldD =>
+  -- Conditional bool fldD =>
+  Conditional (BooleanOf fldD) (BooleanOf fldD) =>
   Untwisted fldD i j ~ g =>
   Field g =>
-  Weierstrass c (Point bool fldC) ->
-  Weierstrass d (Point bool fldD) ->
-  (Weierstrass d (Point bool fldD), g) ->
-  (Weierstrass d (Point bool fldD), g)
+  Weierstrass c (Point fldC) ->
+  Weierstrass d (Point fldD) ->
+  (Weierstrass d (Point fldD), g) ->
+  (Weierstrass d (Point fldD), g)
 additionStep p q (t, f) = (* f) <$> lineFunction p q t
 
 doublingStep ::
   WeierstrassCurve d fldD =>
-  Eq bool fldD =>
+  Eq fldD =>
   Field fldC =>
   Scale fldC fldD =>
-  Conditional bool bool =>
-  Conditional bool fldD =>
+  Conditional (BooleanOf fldD) (BooleanOf fldD) =>
+  BooleanOf fldC ~ BooleanOf fldD =>
   Untwisted fldD i j ~ g =>
   Field g =>
-  Weierstrass c (Point bool fldC) ->
-  (Weierstrass d (Point bool fldD), g) ->
-  (Weierstrass d (Point bool fldD), g)
+  Weierstrass c (Point fldC) ->
+  (Weierstrass d (Point fldD), g) ->
+  (Weierstrass d (Point fldD), g)
 doublingStep p (t, f) = (* f) . (* f) <$> lineFunction p t t
 
 
-lineFunction :: forall c d bool baseFieldC baseFieldD i j g.
+lineFunction :: forall c d baseFieldC baseFieldD i j g.
   WeierstrassCurve d baseFieldD =>
   Field baseFieldC =>
   Scale baseFieldC baseFieldD =>
-  Conditional bool bool =>
-  Conditional bool baseFieldD =>
-  Eq bool baseFieldD =>
+  Conditional (BooleanOf baseFieldD) (BooleanOf baseFieldD) =>
+  -- Conditional bool baseFieldD =>
+  Eq baseFieldD =>
+  BooleanOf baseFieldC ~ BooleanOf baseFieldD =>
   Untwisted baseFieldD i j ~ g =>
-  Weierstrass c (Point bool baseFieldC) ->
-  Weierstrass d (Point bool baseFieldD) ->
-  Weierstrass d (Point bool baseFieldD) ->
-  (Weierstrass d (Point bool baseFieldD), g)
+  Weierstrass c (Point baseFieldC) ->
+  Weierstrass d (Point baseFieldD) ->
+  Weierstrass d (Point baseFieldD) ->
+  (Weierstrass d (Point baseFieldD), g)
 lineFunction
   (Weierstrass (Point x y isInf))
   (Weierstrass (Point x1 y1 isInf1))
   (Weierstrass (Point x2 y2 isInf2)) =
   if isInf || isInf1 || isInf2 then (pointInf, Ext2 (Ext3 one zero zero) zero)
-  else if x1 /= x2 :: bool then (pointXY x3 y3, untwist (negate y) (x `scale` l) (y1 - l * x1))
-  else if y1 + y2 == zero :: bool then (pointInf, untwist x (negate x1) zero)
+  else if x1 /= x2 then (pointXY x3 y3, untwist (negate y) (x `scale` l) (y1 - l * x1))
+  else if y1 + y2 == zero then (pointInf, untwist x (negate x1) zero)
   else (pointXY x3' y3', untwist (negate y) (x `scale` l') (y1 - l' * x1))
   where
     l   = (y2 - y1) // (x2 - x1)
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pasta.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pasta.hs
index 638c1cbec..c0f42aba2 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pasta.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pasta.hs
@@ -40,7 +40,7 @@ type Fq = Zp FqModulus
 instance Field field => WeierstrassCurve "Pasta" field where
   weierstrassB = fromConstant (5 :: Natural)
 
-type Pasta_Point field = Weierstrass "Pasta" (Point Prelude.Bool field)
+type Pasta_Point field = Weierstrass "Pasta" (Point field)
 
 ------------------------------------ Pallas ------------------------------------
 
@@ -73,7 +73,8 @@ instance Scale Fp Vesta_Point where
 instance
   ( Binary field
   , Field field
-  , Eq Prelude.Bool field
+  , Eq field
+  , BooleanOf field ~ Prelude.Bool
   ) => Binary (Pasta_Point field) where
     put (Weierstrass (Point xp yp isInf)) =
       if isInf
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Secp256k1.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Secp256k1.hs
index 78dd32cd3..902804328 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Secp256k1.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Secp256k1.hs
@@ -11,8 +11,6 @@ module ZkFold.Base.Algebra.EllipticCurve.Secp256k1
   , Fp
   ) where
 
-import qualified Prelude
-
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Field
 import           ZkFold.Base.Algebra.Basic.Number
@@ -24,8 +22,8 @@ instance Prime Secp256k1_Scalar
 type Secp256k1_Base = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEFFFFFC2F
 instance Prime Secp256k1_Base
 
-type Secp256k1_Point = Secp256k1_PointOf Prelude.Bool Fp
-type Secp256k1_PointOf bool field = Weierstrass "secp256k1" (Point bool field)
+type Secp256k1_Point = Secp256k1_PointOf Fp
+type Secp256k1_PointOf field = Weierstrass "secp256k1" (Point field)
 
 type Fn = Zp Secp256k1_Scalar
 type Fp = Zp Secp256k1_Base
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/Commit.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/Commit.hs
index 44b93d083..86b949ddc 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/IVC/Commit.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/IVC/Commit.hs
@@ -35,20 +35,20 @@ class PedersonSetup s c where
 type PedersonSetupMaxSize = 100
 
 instance
-  ( CyclicGroup (Weierstrass curve (Point bool field))
-  , Random (ScalarFieldOf (Weierstrass curve (Point bool field)))
-  ) => PedersonSetup [] (Weierstrass curve (Point bool field)) where
+  ( CyclicGroup (Weierstrass curve (Point field))
+  , Random (ScalarFieldOf (Weierstrass curve (Point field)))
+  ) => PedersonSetup [] (Weierstrass curve (Point field)) where
     groupElements =
         -- TODO: This is just for testing purposes! Not to be used in production
-        let x = fst $ random $ mkStdGen 0 :: ScalarFieldOf (Weierstrass curve (Point bool field))
+        let x = fst $ random $ mkStdGen 0 :: ScalarFieldOf (Weierstrass curve (Point field))
         in take (value @PedersonSetupMaxSize) $ iterate (scale x) pointGen
 
 instance
   ( KnownNat n
-  , CyclicGroup (Weierstrass curve (Point bool field))
-  , Random (ScalarFieldOf (Weierstrass curve (Point bool field)))
+  , CyclicGroup (Weierstrass curve (Point field))
+  , Random (ScalarFieldOf (Weierstrass curve (Point field)))
   , n <= PedersonSetupMaxSize
-  ) => PedersonSetup (Vector n) (Weierstrass curve (Point bool field)) where
+  ) => PedersonSetup (Vector n) (Weierstrass curve (Point field)) where
     groupElements =
         -- TODO: This is just for testing purposes! Not to be used in production
         unsafeToVector $ take (value @n) $ groupElements @[]
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs
index 47fb25b80..1a8dc7234 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs
@@ -70,7 +70,7 @@ instance forall p i n l g1 g2 gt (ts :: Type) core .
         , Proof (Plonkup p i n l g1 g2 ts) ~ PlonkupProof g1
         , KnownNat n
         , Foldable l
-        , Compressible Bool g1
+        , Compressible g1
         , Pairing g1 g2 gt
         , Eq gt
         , Arithmetic (ScalarFieldOf g1)
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs
index f12c558bb..492b953d1 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs
@@ -33,7 +33,7 @@ plonkProve :: forall p i n l g1 g2 ts core .
     ( KnownNat n
     , Foldable l
     , Ord (ScalarFieldOf g1)
-    , Compressible Bool g1
+    , Compressible g1
     , ToTranscript ts Word8
     , ToTranscript ts (ScalarFieldOf g1)
     , ToTranscript ts (Compressed g1)
@@ -77,9 +77,9 @@ plonkProve PlonkupProverSetup {..}
         -- Round 2
 
         ts1   = mempty
-            `transcript` compress @Bool cmA
-            `transcript` compress @Bool cmB
-            `transcript` compress @Bool cmC :: ts
+            `transcript` compress cmA
+            `transcript` compress cmB
+            `transcript` compress cmC :: ts
         -- zeta = challenge ts1 :: ScalarFieldOf g1
 
         t_zeta = t relation
@@ -101,9 +101,9 @@ plonkProve PlonkupProverSetup {..}
         -- Round 3
 
         ts2 = ts1
-            -- `transcript` compress @Bool cmF
-            -- `transcript` compress @Bool cmH1
-            -- `transcript` compress @Bool cmH2
+            -- `transcript` compress cmF
+            -- `transcript` compress cmH1
+            -- `transcript` compress cmH2
         beta    = challenge (ts2 `transcript` (1 :: Word8))
         gamma   = challenge (ts2 `transcript` (2 :: Word8))
         delta   = challenge (ts2 `transcript` (3 :: Word8))
@@ -144,8 +144,8 @@ plonkProve PlonkupProverSetup {..}
         -- Round 4
 
         ts3 = ts2
-            `transcript` compress @Bool cmZ1
-            -- `transcript` compress @Bool cmZ2
+            `transcript` compress cmZ1
+            -- `transcript` compress cmZ2
         alpha  = challenge ts3
         alpha2 = alpha * alpha
         -- alpha3 = alpha2 * alpha
@@ -176,9 +176,9 @@ plonkProve PlonkupProverSetup {..}
         -- Round 5
 
         ts4 = ts3
-            `transcript` compress @Bool cmQlow
-            `transcript` compress @Bool cmQmid
-            `transcript` compress @Bool cmQhigh
+            `transcript` compress cmQlow
+            `transcript` compress cmQmid
+            `transcript` compress cmQhigh
         xi = challenge ts4
 
         a_xi    = aX `evalPolyVec` xi
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs
index dbda2b3c8..db72e0afc 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs
@@ -25,7 +25,7 @@ plonkVerify :: forall p i n l g1 g2 gt ts .
     ( KnownNat n
     , Foldable l
     , Pairing g1 g2 gt
-    , Compressible Bool g1
+    , Compressible g1
     , Eq (ScalarFieldOf g1)
     , Eq gt
     , ToTranscript ts Word8
@@ -45,22 +45,22 @@ plonkVerify
         -- Step 4: Compute challenges
 
         ts1   = mempty
-            `transcript` compress @Bool cmA
-            `transcript` compress @Bool cmB
-            `transcript` compress @Bool cmC :: ts
+            `transcript` compress cmA
+            `transcript` compress cmB
+            `transcript` compress cmC :: ts
 
         ts2 = ts1
-            -- `transcript` compress @Bool cmF
-            -- `transcript` compress @Bool cmH1
-            -- `transcript` compress @Bool cmH2
+            -- `transcript` compress cmF
+            -- `transcript` compress cmH1
+            -- `transcript` compress cmH2
         beta    = challenge (ts2 `transcript` (1 :: Word8))
         gamma   = challenge (ts2 `transcript` (2 :: Word8))
         -- delta   = challenge (ts2 `transcript` (3 :: Word8))
         -- epsilon = challenge (ts2 `transcript` (4 :: Word8))
 
         ts3 = ts2
-            `transcript` compress @Bool cmZ1
-            -- `transcript` compress @Bool cmZ2
+            `transcript` compress cmZ1
+            -- `transcript` compress cmZ2
         alpha  = challenge ts3
         alpha2 = alpha * alpha
         -- alpha3 = alpha2 * alpha
@@ -68,9 +68,9 @@ plonkVerify
         -- alpha5 = alpha4 * alpha
 
         ts4 = ts3
-            `transcript` compress @Bool cmQlow
-            `transcript` compress @Bool cmQmid
-            `transcript` compress @Bool cmQhigh
+            `transcript` compress cmQlow
+            `transcript` compress cmQmid
+            `transcript` compress cmQhigh
         xi = challenge ts4
 
         ts5 = ts4
@@ -90,8 +90,8 @@ plonkVerify
         vn i = v ^ (i :: Natural)
 
         ts6 = ts5
-            `transcript` compress @Bool proof1
-            `transcript` compress @Bool proof2
+            `transcript` compress proof1
+            `transcript` compress proof2
         eta = challenge ts6
 
         -- Step 5: Compute zero polynomial evaluation
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs
index 4d038d81d..5e6377b25 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs
@@ -36,7 +36,7 @@ instance forall p i n l g1 g2 gt ts core.
         , Foldable l
         , Ord (Rep i)
         , Pairing g1 g2 gt
-        , Compressible Bool g1
+        , Compressible g1
         , Eq gt
         , Arithmetic (ScalarFieldOf g1)
         , Binary (ScalarFieldOf g2)
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs
index 6561edcae..7103475a1 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs
@@ -36,7 +36,7 @@ plonkupProve :: forall p i n l g1 g2 ts core .
     , KnownNat (PlonkupPolyExtendedLength n)
     , Foldable l
     , Ord (ScalarFieldOf g1)
-    , Compressible Bool g1
+    , Compressible g1
     , ToTranscript ts Word8
     , ToTranscript ts (ScalarFieldOf g1)
     , ToTranscript ts (Compressed g1)
@@ -82,9 +82,9 @@ plonkupProve PlonkupProverSetup {..}
         -- Round 2
 
         ts1   = mempty
-            `transcript` compress @Bool cmA
-            `transcript` compress @Bool cmB
-            `transcript` compress @Bool cmC :: ts
+            `transcript` compress cmA
+            `transcript` compress cmB
+            `transcript` compress cmC :: ts
         -- zeta = challenge ts1 :: ScalarFieldOf g1
 
         t_zeta = t relation
@@ -106,9 +106,9 @@ plonkupProve PlonkupProverSetup {..}
         -- Round 3
 
         ts2 = ts1
-            `transcript` compress @Bool cmF
-            `transcript` compress @Bool cmH1
-            `transcript` compress @Bool cmH2
+            `transcript` compress cmF
+            `transcript` compress cmH1
+            `transcript` compress cmH2
         beta    = challenge (ts2 `transcript` (1 :: Word8))
         gamma   = challenge (ts2 `transcript` (2 :: Word8))
         delta   = challenge (ts2 `transcript` (3 :: Word8))
@@ -149,8 +149,8 @@ plonkupProve PlonkupProverSetup {..}
         -- Round 4
 
         ts3 = ts2
-            `transcript` compress @Bool cmZ1
-            `transcript` compress @Bool cmZ2
+            `transcript` compress cmZ1
+            `transcript` compress cmZ2
         alpha  = challenge ts3
         alpha2 = alpha * alpha
         alpha3 = alpha2 * alpha
@@ -181,9 +181,9 @@ plonkupProve PlonkupProverSetup {..}
         -- Round 5
 
         ts4 = ts3
-            `transcript` compress @Bool cmQlow
-            `transcript` compress @Bool cmQmid
-            `transcript` compress @Bool cmQhigh
+            `transcript` compress cmQlow
+            `transcript` compress cmQmid
+            `transcript` compress cmQhigh
         xi = challenge ts4
 
         a_xi    = aX `evalPolyVec` xi
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs
index 521889d14..be610331a 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs
@@ -28,7 +28,7 @@ plonkupVerify :: forall p i n l g1 g2 gt ts .
     , KnownNat (PlonkupPolyExtendedLength n)
     , Foldable l
     , Pairing g1 g2 gt
-    , Compressible Bool g1
+    , Compressible g1
     , Eq (ScalarFieldOf g1)
     , Eq gt
     , ToTranscript ts Word8
@@ -48,22 +48,22 @@ plonkupVerify
         -- Step 4: Compute challenges
 
         ts1   = mempty
-            `transcript` compress @Bool cmA
-            `transcript` compress @Bool cmB
-            `transcript` compress @Bool cmC :: ts
+            `transcript` compress cmA
+            `transcript` compress cmB
+            `transcript` compress cmC :: ts
 
         ts2 = ts1
-            `transcript` compress @Bool cmF
-            `transcript` compress @Bool cmH1
-            `transcript` compress @Bool cmH2
+            `transcript` compress cmF
+            `transcript` compress cmH1
+            `transcript` compress cmH2
         beta    = challenge (ts2 `transcript` (1 :: Word8))
         gamma   = challenge (ts2 `transcript` (2 :: Word8))
         delta   = challenge (ts2 `transcript` (3 :: Word8))
         epsilon = challenge (ts2 `transcript` (4 :: Word8))
 
         ts3 = ts2
-            `transcript` compress @Bool cmZ1
-            `transcript` compress @Bool cmZ2
+            `transcript` compress cmZ1
+            `transcript` compress cmZ2
         alpha  = challenge ts3
         alpha2 = alpha * alpha
         alpha3 = alpha2 * alpha
@@ -71,9 +71,9 @@ plonkupVerify
         alpha5 = alpha4 * alpha
 
         ts4 = ts3
-            `transcript` compress @Bool cmQlow
-            `transcript` compress @Bool cmQmid
-            `transcript` compress @Bool cmQhigh
+            `transcript` compress cmQlow
+            `transcript` compress cmQmid
+            `transcript` compress cmQhigh
         xi = challenge ts4
 
         ts5 = ts4
@@ -93,8 +93,8 @@ plonkupVerify
         vn i = v ^ (i :: Natural)
 
         ts6 = ts5
-            `transcript` compress @Bool proof1
-            `transcript` compress @Bool proof2
+            `transcript` compress proof1
+            `transcript` compress proof2
         eta = challenge ts6
 
         -- Step 5: Compute zero polynomial evaluation
diff --git a/symbolic-base/src/ZkFold/Symbolic/Algorithms/ECDSA/ECDSA.hs b/symbolic-base/src/ZkFold/Symbolic/Algorithms/ECDSA/ECDSA.hs
index 44436eb6f..97a8894e5 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Algorithms/ECDSA/ECDSA.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Algorithms/ECDSA/ECDSA.hs
@@ -25,7 +25,7 @@ ecdsaVerify
      , KnownNat n
      , baseField ~ UInt 256 'Auto c
      , ScalarFieldOf point ~ FieldElement c
-     , point ~ Weierstrass curve (Point (Bool c) baseField)
+     , point ~ Weierstrass curve (Point baseField)
      , CyclicGroup point
      , SemiEuclidean (UInt 256 'Auto c)
      , KnownNat (NumberOfRegisters (S.BaseField c) 256 'Auto)
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs b/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
index 3f14c8e75..1514deaa1 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
@@ -72,7 +72,7 @@ deriving stock instance Haskell.Show (c (Vector n)) => Haskell.Show (ByteString
 deriving stock instance Haskell.Eq (c (Vector n)) => Haskell.Eq (ByteString n c)
 deriving anyclass instance NFData (c (Vector n)) => NFData (ByteString n c)
 deriving newtype instance (KnownNat n, Symbolic c) => SymbolicData (ByteString n c)
-deriving newtype instance (Symbolic c, KnownNat n) => Eq (Bool c) (ByteString n c)
+deriving newtype instance (Symbolic c, KnownNat n) => Eq (ByteString n c)
 deriving newtype instance (Symbolic c, KnownNat n) => Conditional (Bool c) (ByteString n c)
 
 instance
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
index 3f09e7223..b2e1ea120 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
@@ -61,9 +61,8 @@ instance Symbolic c => Conditional (Bool c) (Proxy c) where
   bool _ _ _ = Proxy
 
 instance Conditional Prelude.Bool Prelude.Bool where bool = H.bool
-
 instance Conditional Prelude.Bool Prelude.String where bool = H.bool
-
+instance Conditional Prelude.Bool Natural where bool = H.bool
 instance Conditional Prelude.Bool (Zp n) where bool = H.bool
 
 instance (KnownNat n, Conditional bool x) => Conditional bool (Vector n x) where
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
index 86b15adde..4cac62fdf 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
@@ -5,6 +5,7 @@
 module ZkFold.Symbolic.Data.Eq (
     Eq(..),
     elem,
+    SymbolicEq,
     GEq (..)
 ) where
 
@@ -23,39 +24,54 @@ import           ZkFold.Base.Algebra.Basic.Number
 import           ZkFold.Base.Data.Package
 import           ZkFold.Base.Data.Vector
 import           ZkFold.Symbolic.Class
+import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Bool        (Bool (Bool), BoolType (..), all, any)
 import           ZkFold.Symbolic.Data.Combinators (runInvert)
+import           ZkFold.Symbolic.Data.Conditional (Conditional, GConditional)
 import           ZkFold.Symbolic.MonadCircuit
 
-class Eq b a where
+class Conditional (BooleanOf a) a => Eq a where
+
+    type BooleanOf a
+    type BooleanOf a = GBooleanOf (G.Rep a)
+
     infix 4 ==
-    (==) :: a -> a -> b
-    default (==) :: (G.Generic a, GEq b (G.Rep a)) => a -> a -> b
+    (==) :: a -> a -> BooleanOf a
+    default (==)
+      :: (G.Generic a, GEq (G.Rep a), BooleanOf a ~ GBooleanOf (G.Rep a))
+      => a -> a -> BooleanOf a
     x == y = geq (G.from x) (G.from y)
 
     infix 4 /=
-    (/=) :: a -> a -> b
-    default (/=) :: (G.Generic a, GEq b (G.Rep a)) => a -> a -> b
+    (/=) :: a -> a -> BooleanOf a
+    default (/=)
+      :: (G.Generic a, GEq (G.Rep a), BooleanOf a ~ GBooleanOf (G.Rep a))
+      => a -> a -> BooleanOf a
     x /= y = gneq (G.from x) (G.from y)
 
-elem :: (BoolType b, Eq b a, Foldable t) => a -> t a -> b
+elem :: (Eq a, Foldable t) => a -> t a -> BooleanOf a
 elem x = any (== x)
 
-instance Eq Haskell.Bool Natural where
+instance Eq Natural where
+    type BooleanOf Natural = Haskell.Bool
     (==) = (Haskell.==)
     (/=) = (Haskell./=)
-instance Eq Haskell.Bool Haskell.Bool where
+instance Eq Haskell.Bool where
+    type BooleanOf Haskell.Bool = Haskell.Bool
     (==) = (Haskell.==)
     (/=) = (Haskell./=)
-instance Eq Haskell.Bool Haskell.String where
+instance Eq Haskell.String where
+    type BooleanOf Haskell.String = Haskell.Bool
     (==) = (Haskell.==)
     (/=) = (Haskell./=)
-instance KnownNat n => Eq Haskell.Bool (Zp n) where
+instance KnownNat n => Eq (Zp n) where
+    type BooleanOf (Zp n) = Haskell.Bool
     (==) = (Haskell.==)
     (/=) = (Haskell./=)
 
 instance (Symbolic c, Haskell.Eq (BaseField c), Representable f, Traversable f)
-  => Eq (Bool c) (c f) where
+  => Eq (c f) where
+    type BooleanOf (c f) = Bool c
     x == y =
         let
             result = symbolic2F x y
@@ -83,31 +99,51 @@ instance (Symbolic c, Haskell.Eq (BaseField c), Representable f, Traversable f)
         in
             any Bool (unpacked result)
 
-instance (BoolType b, Eq b x) => Eq b (Vector n x) where
+type SymbolicEq x =
+  ( SymbolicOutput x
+  , Eq x
+  , BooleanOf x ~ Bool (Context x)
+  )
+
+instance (KnownNat n, Eq x) => Eq (Vector n x) where
+    type BooleanOf (Vector n x) = BooleanOf x
     u == v = V.foldl (&&) true (V.zipWith (==) (toV u) (toV v))
     u /= v = V.foldl (||) false (V.zipWith (/=) (toV u) (toV v))
 
-deriving newtype instance Symbolic c => Eq (Bool c) (Bool c)
-
-instance (BoolType b, Eq b x0, Eq b x1) => Eq b (x0,x1)
-instance (BoolType b, Eq b x0, Eq b x1, Eq b x2) => Eq b (x0,x1,x2)
-instance (BoolType b, Eq b x0, Eq b x1, Eq b x2, Eq b x3) => Eq b (x0,x1,x2,x3)
-
-instance (BoolType bool, Eq bool field) => Eq bool (Ext2 field i)
-instance (BoolType bool, Eq bool field) => Eq bool (Ext3 field i)
-
-class GEq b u where
-    geq :: u x -> u x -> b
-    gneq :: u x -> u x -> b
-
-instance (BoolType b, GEq b u, GEq b v) => GEq b (u G.:*: v) where
+deriving newtype instance Symbolic c => Eq (Bool c)
+
+instance (Eq x0, Eq x1, BooleanOf x0 ~ BooleanOf x1) => Eq (x0,x1)
+instance
+  ( Eq x0, Eq x1, Eq x2
+  , BooleanOf x0 ~ BooleanOf x1
+  , BooleanOf x1 ~ BooleanOf x2
+  ) => Eq (x0,x1,x2)
+instance
+  ( Eq x0, Eq x1, Eq x2, Eq x3
+  , BooleanOf x0 ~ BooleanOf x1
+  , BooleanOf x1 ~ BooleanOf x2
+  , BooleanOf x2 ~ BooleanOf x3
+  ) => Eq (x0,x1,x2,x3)
+
+instance Eq field => Eq (Ext2 field i)
+instance Eq field => Eq (Ext3 field i)
+
+class GConditional (GBooleanOf u) u => GEq u where
+    type GBooleanOf u
+    geq :: u x -> u x -> GBooleanOf u
+    gneq :: u x -> u x -> GBooleanOf u
+
+instance (GBooleanOf u ~ GBooleanOf v, GEq u, GEq v) => GEq (u G.:*: v) where
+    type GBooleanOf (u G.:*: v) = GBooleanOf u
     geq (x0 G.:*: x1) (y0 G.:*: y1) = geq x0 y0 && geq x1 y1
     gneq (x0 G.:*: x1) (y0 G.:*: y1) = gneq x0 y0 || gneq x1 y1
 
-instance GEq b v => GEq b (G.M1 i c v) where
+instance GEq v => GEq (G.M1 i c v) where
+    type GBooleanOf (G.M1 i c v) = GBooleanOf v
     geq (G.M1 x) (G.M1 y) = geq x y
     gneq (G.M1 x) (G.M1 y) = gneq x y
 
-instance Eq b x => GEq b (G.Rec0 x) where
+instance Eq x => GEq (G.Rec0 x) where
+    type GBooleanOf (G.Rec0 x) = BooleanOf x
     geq (G.K1 x) (G.K1 y) = x == y
     gneq (G.K1 x) (G.K1 y) = x /= y
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/FFA.hs b/symbolic-base/src/ZkFold/Symbolic/Data/FFA.hs
index 9213edde8..2658cd872 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/FFA.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/FFA.hs
@@ -213,7 +213,7 @@ instance Finite (Zp p) => Finite (FFA p b) where
   type Order (FFA p b) = p
 
 -- FIXME: This Eq instance is wrong
-deriving newtype instance Symbolic c => Eq (Bool c) (FFA p c)
+deriving newtype instance Symbolic c => Eq (FFA p c)
 
 deriving newtype instance (Symbolic c, b ~ Bool c) => Conditional b (FFA p c)
 
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs b/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
index cd49ba674..92166c817 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
@@ -42,7 +42,7 @@ deriving newtype instance Symbolic c => SymbolicData (FieldElement c)
 
 deriving newtype instance Symbolic c => Conditional (Bool c) (FieldElement c)
 
-deriving newtype instance Symbolic c => Eq (Bool c) (FieldElement c)
+deriving newtype instance Symbolic c => Eq (FieldElement c)
 
 deriving newtype instance Symbolic c => Ord (Bool c) (FieldElement c)
 
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Hash.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Hash.hs
index aab883ff4..3dc4098b0 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Hash.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Hash.hs
@@ -14,7 +14,7 @@ import           ZkFold.Base.Control.HApplicative (hunit)
 import           ZkFold.Symbolic.Class            (Symbolic (fromCircuitF, witnessF), fromCircuit2F)
 import           ZkFold.Symbolic.Data.Bool        (Bool (..))
 import           ZkFold.Symbolic.Data.Class       (SymbolicData (..), SymbolicOutput)
-import           ZkFold.Symbolic.Data.Eq          (Eq, (==))
+import           ZkFold.Symbolic.Data.Eq          (SymbolicEq, (==))
 import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
 import           ZkFold.Symbolic.Data.Payloaded   (Payloaded (Payloaded))
 import           ZkFold.Symbolic.MonadCircuit     (constraint, unconstrained)
@@ -48,7 +48,7 @@ hash a = Hash (hasher a) $
 preimage ::
   forall h a c .
   ( Hashable h a, SymbolicOutput a, Context h ~ c, Context a ~ c
-  , Eq (Bool c) h) => Hash h a -> a
+  , SymbolicEq h) => Hash h a -> a
 preimage Hash {..} =
   let Payloaded (l :*: p) = hValue
       raw :: a = restore $ const
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/List.hs b/symbolic-base/src/ZkFold/Symbolic/Data/List.hs
index 2b8e2b28f..8561f4af4 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/List.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/List.hs
@@ -24,6 +24,8 @@ import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool        (Bool (..))
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Combinators
+import           ZkFold.Symbolic.Data.Conditional (Conditional)
+import           ZkFold.Symbolic.Data.Eq          (Eq)
 import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
 import           ZkFold.Symbolic.Data.Payloaded   (Payloaded (Payloaded))
 import           ZkFold.Symbolic.Data.UInt        (UInt)
@@ -51,6 +53,8 @@ data List c x = List
 instance (SymbolicData x, c ~ Context x) => SymbolicData (List c x)
 -- | TODO: Maybe some 'isValid' check for Lists?..
 instance (SymbolicInput x, c ~ Context x) => SymbolicInput (List c x)
+instance (SymbolicInput x, c ~ Context x) => Conditional (Bool c) (List c x)
+instance (SymbolicInput x, c ~ Context x) => Eq (List c x)
 
 -- | TODO: A proof-of-concept where hash == id.
 -- Replace id with a proper hash if we need lists to be cryptographically secure.
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Maybe.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Maybe.hs
index b7753d9f7..069289d6c 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Maybe.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Maybe.hs
@@ -32,7 +32,7 @@ deriving stock instance (Haskell.Eq (context Par1), Haskell.Eq x) => Haskell.Eq
 
 instance (SymbolicOutput x, Context x ~ c) => SymbolicData (Maybe c x) where
 instance (SymbolicOutput x, Context x ~ c, Conditional (Bool c) x) => Conditional (Bool c) (Maybe c x)
-instance (SymbolicOutput x, Context x ~ c, Eq (Bool c) x) => Eq (Bool c) (Maybe c x)
+instance (Context x ~ c, SymbolicEq x) => Eq (Maybe c x)
 
 just :: Symbolic c => x -> Maybe c x
 just = Maybe true
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Secp256k1.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Secp256k1.hs
index 30a8e7ccc..1137c5e7b 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Secp256k1.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Secp256k1.hs
@@ -20,7 +20,7 @@ import           ZkFold.Symbolic.Data.Conditional
 import           ZkFold.Symbolic.Data.FFA
 import           ZkFold.Symbolic.Data.FieldElement
 
-type Secp256k1_Point ctx = Secp256k1_PointOf (Bool ctx) (FFA Secp256k1_Base ctx)
+type Secp256k1_Point ctx = Secp256k1_PointOf (FFA Secp256k1_Base ctx)
 
 instance Symbolic ctx => CyclicGroup (Secp256k1_Point ctx) where
   type ScalarFieldOf (Secp256k1_Point ctx) = FieldElement ctx
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs b/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
index 7c9639101..18b6f6fb0 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
@@ -65,7 +65,7 @@ deriving instance (Haskell.Eq (context (Vector (NumberOfRegisters (BaseField con
 deriving instance (Haskell.Show (BaseField context), Haskell.Show (context (Vector (NumberOfRegisters (BaseField context) n r)))) => Haskell.Show (UInt n r context)
 deriving newtype instance (KnownRegisters c n r, Symbolic c) => SymbolicData (UInt n r c)
 deriving newtype instance (KnownRegisters c n r, Symbolic c) => Conditional (Bool c) (UInt n r c)
-deriving newtype instance (KnownRegisters c n r, Symbolic c) => Eq (Bool c) (UInt n r c)
+deriving newtype instance (KnownRegisters c n r, Symbolic c) => Eq (UInt n r c)
 
 instance (Symbolic c, KnownNat n, KnownRegisterSize r) => FromConstant Natural (UInt n r c) where
     fromConstant c = UInt . embed @c $ naturalToVector @c @n @r c
@@ -167,9 +167,8 @@ eea
     .  Symbolic c
     => SemiEuclidean (UInt n r c)
     => KnownNat n
-    => KnownRegisters c n r
     => AdditiveGroup (UInt n r c)
-    => Eq (Bool c) (UInt n r c)
+    => Eq (UInt n r c)
     => UInt n r c -> UInt n r c -> (UInt n r c, UInt n r c, UInt n r c)
 eea a b = eea' 1 a b one zero zero one
     where
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/ZkPass.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/ZkPass.hs
index 4bf5352bb..cb5d51d77 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/ZkPass.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/ZkPass.hs
@@ -51,7 +51,7 @@ verifyAllocatorSignature :: forall point n context curve baseField.
      , KnownNat n
      , baseField ~ UInt 256 'Auto context
      , ScalarFieldOf point ~ FieldElement context
-     , point ~ Weierstrass curve (Point (Bool context) baseField)
+     , point ~ Weierstrass curve (Point baseField)
      , CyclicGroup point
      , SemiEuclidean (UInt 256 'Auto context)
      , KnownNat (NumberOfRegisters (S.BaseField context) 256 'Auto)
@@ -84,7 +84,7 @@ verifyValidatorSignature :: forall point n context curve baseField.
      , KnownNat n
      , baseField ~ UInt 256 'Auto context
      , ScalarFieldOf point ~ FieldElement context
-     , point ~ Weierstrass curve (Point (Bool context) baseField)
+     , point ~ Weierstrass curve (Point baseField)
      , CyclicGroup point
      , SemiEuclidean (UInt 256 'Auto context)
      , KnownNat (NumberOfRegisters (S.BaseField context) 256 'Auto)
@@ -131,7 +131,7 @@ zkPassSymbolicVerifier :: forall point n context curve baseField.
      , KnownNat n
      , baseField ~ UInt 256 'Auto context
      , ScalarFieldOf point ~ FieldElement context
-     , point ~ Weierstrass curve (Point (Bool context) baseField)
+     , point ~ Weierstrass curve (Point baseField)
      , CyclicGroup point
      , SemiEuclidean (UInt 256 'Auto context)
      , KnownNat (NumberOfRegisters (S.BaseField context) 256 'Auto)
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
index 98a7676ad..5b76eb88c 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
@@ -28,7 +28,7 @@ data Address context = Address {
 deriving instance (Haskell.Eq (ByteString 4 context), Haskell.Eq (ByteString 224 context))
     => Haskell.Eq (Address context)
 
-instance Symbolic context => Eq (Bool context) (Address context)
+instance Symbolic context => Eq (Address context)
 instance Symbolic context => Conditional (Bool context) (Address context)
 instance Symbolic context => SymbolicData (Address context)
 instance Symbolic context => SymbolicInput (Address context) where
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs
index 056b3f341..7b5df16fe 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs
@@ -39,7 +39,7 @@ instance
     , KnownNat tokens
     , KnownRegisters context 32 Auto
     , KnownRegisters context 64 Auto
-    ) => Eq (Bool context) (Input tokens datum context)
+    ) => Eq (Input tokens datum context)
 
 deriving instance
     ( Haskell.Eq (OutputRef context)
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs
index ee8debfe8..ec043491c 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs
@@ -74,5 +74,5 @@ instance
     ( Symbolic context
     , KnownNat tokens
     , KnownRegisters context 64 Auto
-    ) => Eq (Bool context) (Output tokens datum context)
+    ) => Eq (Output tokens datum context)
 
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs
index f5b2ba061..eecc3c1f1 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs
@@ -40,4 +40,4 @@ instance (Symbolic context, KnownRegisters context 32 Auto)
     => Conditional (Bool context) (OutputRef context) where
 
 instance (Symbolic context, KnownRegisters context 32 Auto)
-    => Eq (Bool context) (OutputRef context) where
+    => Eq (OutputRef context) where
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
index 30a1ee7f4..01d2c1802 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
@@ -38,7 +38,8 @@ deriving instance (Symbolic context, KnownNat n, KnownRegisters context 64 Auto)
 deriving newtype instance
   ( Symbolic context
   , KnownRegisters context 64 Auto
-  ) => Eq (Bool context) (Value n context)
+  , KnownNat n
+  ) => Eq (Value n context)
 
 deriving newtype instance
   ( Symbolic context
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Wrapper.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Wrapper.hs
index 9c696c65d..60c6c5cbd 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Wrapper.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Wrapper.hs
@@ -18,7 +18,7 @@ type Contract tx redeemer context = tx context -> redeemer context -> Bool conte
 
 -- | Wrap the contract, exposing the transaction hash as the single public input.
 symbolicContractWrapper :: forall inputs rinputs outputs tokens mint datum redeemer context .
-    (Symbolic context, Eq (Bool context) (TxHash context))
+    (Symbolic context, Eq (TxHash context))
     => Contract (Transaction inputs rinputs outputs tokens mint datum) redeemer context
     -> TxHash context
     -> Transaction inputs rinputs outputs tokens mint datum context
diff --git a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types.hs b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types.hs
index 283693a54..b0c691bc2 100644
--- a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types.hs
+++ b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types.hs
@@ -56,19 +56,19 @@ type Signature context =
     , AdditiveMonoid (UInt 32 Auto context)
     , AdditiveMonoid (Value context)
     , Conditional (Bool context) (Update context)
-    , Eq (Bool context) (Hash context)
-    , Eq (Bool context) (Input context)
-    , Eq (Bool context) (Address context, Datum context)
-    , Eq (Bool context) (CurrencySymbol context, Token context)
-    , Eq (Bool context) (Update context)
-    , Eq (Bool context) (Value context)
-    , Eq (Bool context) (List context (Hash context))
-    , Eq (Bool context) (List context (Address context, Datum context))
-    , Eq (Bool context) (List context (ContractId context, Token context))
-    , Eq (Bool context) (List context (Input context))
-    , Eq (Bool context) (Output context)
-    , Eq (Bool context) (List context (Transaction context))
-    , Eq (Bool context) (List context (List context (TransactionId context)))
+    , Eq (Hash context)
+    , Eq (Input context)
+    , Eq (Address context, Datum context)
+    , Eq (CurrencySymbol context, Token context)
+    , Eq (Update context)
+    , Eq (Value context)
+    , Eq (List context (Hash context))
+    , Eq (List context (Address context, Datum context))
+    , Eq (List context (ContractId context, Token context))
+    , Eq (List context (Input context))
+    , Eq (Output context)
+    , Eq (List context (Transaction context))
+    , Eq (List context (List context (TransactionId context)))
     , Foldable (List context)
     , Functor (List context)
     , MultiplicativeMonoid (UInt 32 Auto context)
diff --git a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Address.hs b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Address.hs
index 5081b7332..8ec1fc896 100644
--- a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Address.hs
+++ b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Address.hs
@@ -3,9 +3,10 @@ module ZkFold.Symbolic.Ledger.Types.Address where
 import           Prelude                               hiding (Bool, Eq, length, splitAt, (*), (+))
 
 import           ZkFold.Symbolic.Ledger.Types.Contract (Contract, ContractId)
+import           ZkFold.Symbolic.Data.FieldElement     (FieldElement)
 
 -- | Input to the spending contract. Usually some sort of commitment information to be used when spending the output.
-data Datum context
+type Datum = FieldElement
 
 -- | A contract that locks a transaction output.
 -- In order to spend the output, the spending transaction must satisfy the contract.
diff --git a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Hash.hs b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Hash.hs
index c279700b4..9d678dbff 100644
--- a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Hash.hs
+++ b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Hash.hs
@@ -2,8 +2,10 @@ module ZkFold.Symbolic.Ledger.Types.Hash where
 
 import           Prelude hiding (Bool, Eq, length, splitAt, (*), (+))
 
+import           ZkFold.Symbolic.Data.FieldElement (FieldElement)
+
 -- | Hash type used in the zkFold ledger.
-data Hash context
+type Hash = FieldElement
 
 class Hashable context x where
   hash :: x -> Hash context
diff --git a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Output.hs b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Output.hs
index 607d5273d..777b564aa 100644
--- a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Output.hs
+++ b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Output.hs
@@ -1,7 +1,16 @@
+{-# LANGUAGE UndecidableInstances #-}
+
 module ZkFold.Symbolic.Ledger.Types.Output where
 
+import           GHC.Generics                         (Generic)
 import           Prelude                              hiding (Bool, Eq, length, splitAt, (*), (+))
 
+import           ZkFold.Symbolic.Class                (Symbolic)
+import           ZkFold.Symbolic.Data.Bool            (Bool)
+import           ZkFold.Symbolic.Data.Class           (SymbolicData)
+import           ZkFold.Symbolic.Data.Combinators     (KnownRegisters, RegisterSize (Auto))
+import           ZkFold.Symbolic.Data.Conditional     (Conditional)
+import           ZkFold.Symbolic.Data.Eq              (Eq)
 import           ZkFold.Symbolic.Ledger.Types.Address (Address, Datum)
 import           ZkFold.Symbolic.Ledger.Types.Value   (Value)
 
@@ -13,4 +22,8 @@ data Output context = Output
         -- ^ Value locked by the output
         , txoDatum   :: Datum context
         -- ^ Datum associated with the output
-        }
+        } deriving Generic
+
+instance (Symbolic context, KnownRegisters context 64 Auto) => SymbolicData (Output context)
+instance (Symbolic context, KnownRegisters context 64 Auto) => Conditional (Bool context) (Output context)
+instance (Symbolic context, KnownRegisters context 64 Auto) => Eq (Output context)
diff --git a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Update.hs b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Update.hs
index 18a6f92b1..c7f72510e 100644
--- a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Update.hs
+++ b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Update.hs
@@ -64,7 +64,6 @@ emptyUpdate ::
   => Context (AddressIndex context) ~ context
   => Context (ContractData context) ~ context
   => Context (Input context) ~ context
-  => Context (Output context) ~ context
   => Hash context
   -> Update context
 emptyUpdate prev = Update
diff --git a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Value.hs b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Value.hs
index 85c87f8ce..37ba15d53 100644
--- a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Value.hs
+++ b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Value.hs
@@ -1,22 +1,25 @@
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Symbolic.Ledger.Types.Value where
 
+import           GHC.Generics                          (Generic)
 import           Prelude                               hiding (Bool, Eq, all, length, null, splitAt, (*), (+), (==))
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Symbolic.Class                 (Symbolic)
 import           ZkFold.Symbolic.Data.Bool             (Bool)
 import           ZkFold.Symbolic.Data.Class            (SymbolicData (..), SymbolicOutput)
-import           ZkFold.Symbolic.Data.Combinators      (RegisterSize (Auto))
+import           ZkFold.Symbolic.Data.Combinators      (KnownRegisters, RegisterSize (Auto))
 import           ZkFold.Symbolic.Data.Conditional      (Conditional, bool)
-import           ZkFold.Symbolic.Data.Eq               (Eq ((==)))
+import           ZkFold.Symbolic.Data.Eq               (Eq ((==)), SymbolicEq)
+import           ZkFold.Symbolic.Data.FieldElement     (FieldElement)
 import           ZkFold.Symbolic.Data.List             (List, emptyList, null, singleton, uncons, (.:))
 import           ZkFold.Symbolic.Data.UInt             (UInt)
 import           ZkFold.Symbolic.Ledger.Types.Contract (Contract, ContractId)
 
 -- | Input to the minting contract. Usually a token name.
-data Token context
+type Token = FieldElement
 
 -- | A minting contract is a contract that guards the minting and burning of tokens.
 -- In order to mint or burn tokens, the transaction must satisfy the minting contract.
@@ -32,7 +35,11 @@ data Value context = Value
   { mintingPolicy :: CurrencySymbol context
   , tokenInstance :: Token context
   , tokenQuantity :: UInt 64 Auto context
-  }
+  } deriving Generic
+
+instance (Symbolic context, KnownRegisters context 64 Auto) => SymbolicData (Value context)
+instance (Symbolic context, KnownRegisters context 64 Auto) => Conditional (Bool context) (Value context)
+instance (Symbolic context, KnownRegisters context 64 Auto) => Eq (Value context)
 
 newtype MultiAssetValue context = UnsafeMultiAssetValue (List context (Value context))
 
@@ -48,7 +55,8 @@ addValue ::
   => Symbolic context
   => SymbolicOutput (Value context)
   => Context (Value context) ~ context
-  => Eq (Bool context) (CurrencySymbol context)
+  => SymbolicEq (CurrencySymbol context)
+  => Context (CurrencySymbol context) ~ context
   => Value context
   -> MultiAssetValue context
   -> MultiAssetValue context
@@ -69,7 +77,8 @@ multiValueAsset ::
   => SymbolicOutput (Value context)
   => Context (Value context) ~ context
   => Conditional (Bool context) (MultiAssetValue context)
-  => Eq (Bool context) (CurrencySymbol context)
+  => SymbolicEq (CurrencySymbol context)
+  => Context (CurrencySymbol context) ~ context
   => Foldable (List context)
   => List context (Value context)
   -> MultiAssetValue context
diff --git a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs
index f636c8ab8..4a5eedf64 100644
--- a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs
+++ b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs
@@ -84,7 +84,7 @@ updateIsValid ::
   => Context (Output context) ~ context
   => Context (ContractData context) ~ context
   => Context (Value context) ~ context
-  => Eq (Bool context) (MultiAssetValue context)
+  => Eq (MultiAssetValue context)
   => Conditional (Bool context) (MultiAssetValue context)
   => Hash context
   -> Update context