diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,7 @@
+## 0.7.0 (2024-10-11)
+* add predicate simplifier at `Rerefined.Simplify`
+  * old "normalizer" stuff removed
+
 ## 0.6.0 (2024-10-01)
 * remove `Via` predicate, only need `validateVia`
 * swap `validateBool` args
diff --git a/rerefined.cabal b/rerefined.cabal
--- a/rerefined.cabal
+++ b/rerefined.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           rerefined
-version:        0.6.0
+version:        0.7.0
 synopsis:       Refinement types, again
 description:    Please see README.md.
 category:       Types, Data
@@ -40,11 +40,9 @@
       Rerefined.Predicate.Logical.Iff
       Rerefined.Predicate.Logical.Nand
       Rerefined.Predicate.Logical.Nor
-      Rerefined.Predicate.Logical.Normalize
       Rerefined.Predicate.Logical.Not
       Rerefined.Predicate.Logical.Or
       Rerefined.Predicate.Logical.Xor
-      Rerefined.Predicate.Normalize
       Rerefined.Predicate.Relational
       Rerefined.Predicate.Relational.Internal
       Rerefined.Predicate.Relational.Length
@@ -55,6 +53,8 @@
       Rerefined.Predicates.Operators
       Rerefined.Refine
       Rerefined.Refine.TH
+      Rerefined.Simplify
+      Rerefined.Simplify.Relational
   other-modules:
       Paths_rerefined
   hs-source-dirs:
diff --git a/src/Rerefined/Predicate/Logical/Normalize.hs b/src/Rerefined/Predicate/Logical/Normalize.hs
deleted file mode 100644
--- a/src/Rerefined/Predicate/Logical/Normalize.hs
+++ /dev/null
@@ -1,10 +0,0 @@
-module Rerefined.Predicate.Logical.Normalize where
-
-import Rerefined.Predicate.Logical
-
-type family NormLogi p where
-    NormLogi (Not (Not p)) = Just p
-    NormLogi (Or   l l)    = Just l
-    NormLogi (And  l l)    = Just l
-    NormLogi (Nand l l)    = Just (Not l)
-    NormLogi p             = Nothing
diff --git a/src/Rerefined/Predicate/Normalize.hs b/src/Rerefined/Predicate/Normalize.hs
deleted file mode 100644
--- a/src/Rerefined/Predicate/Normalize.hs
+++ /dev/null
@@ -1,12 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-
-module Rerefined.Predicate.Normalize where
-
-import Rerefined.Predicate.Logical.Normalize
-
-type family Norm p where
-    Norm p = Norm' p (NormLogi p)
-
-type family Norm' p mp where
-    Norm' p Nothing   = p
-    Norm' p (Just p') = Norm p'
diff --git a/src/Rerefined/Predicate/Relational.hs b/src/Rerefined/Predicate/Relational.hs
--- a/src/Rerefined/Predicate/Relational.hs
+++ b/src/Rerefined/Predicate/Relational.hs
@@ -1,8 +1,10 @@
 module Rerefined.Predicate.Relational
-  ( CompareValue
+  ( RelOp(..)
+  , CompareValue
   , Sign(..)
   , CompareLength
-  , LTE, GTE
+  , WidenRelOp
+  , FlipRelOp
   ) where
 
 import Rerefined.Predicate.Relational.Internal
diff --git a/src/Rerefined/Predicate/Relational/Internal.hs b/src/Rerefined/Predicate/Relational/Internal.hs
--- a/src/Rerefined/Predicate/Relational/Internal.hs
+++ b/src/Rerefined/Predicate/Relational/Internal.hs
@@ -1,111 +1,87 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}  -- for ReifyRelOp
 {-# LANGUAGE UndecidableInstances #-} -- for WidenRelOp
 
-{- | Relational operator definitions.
-
-Haskell base exports the type 'Ordering', which is an enum that states the
-result of comparing two 'Ord's. We can utilize this to define /relational
-operators/:
-
-* 'LT', 'EQ' and 'GT' already map to relational operators.
-* The others can be defined by combining the above with 'Or'. e.g. @'LT' ``Or``
-  'EQ'@ -> "less than or equal" ('<=')
-
-What's the point? We save on definitions, and get to reuse well-known data types
-which most users will have intuition for. We do have to contest with
-commutativity, but this is an extremely minor concern which can only come up if
-you don't use the provided type synonyms, or do lots of type-level predicate
-manipulation. And we provide those swapped-order instances anyway!
--}
+-- | Relational operator definitions.
 
 module Rerefined.Predicate.Relational.Internal where
 
-import Rerefined.Predicate.Logical.Or
 import GHC.TypeNats
 import Data.Type.Ord ( OrdCond )
 import GHC.TypeLits ( Symbol )
 
-import Data.Kind ( Type )
-
-type LTE = LT `Or` EQ
+{- | Relational operator.
 
--- | "not equal to" is equivalent to "strictly less than or greater than". We
---   could use 'Rerefined.Predicate.Logical.Not.Not', but sticking with just
---   'Or' keeps the internals simple.
-type NEQ = LT `Or` GT
+Constructor order is arbitrary due to @NEQ@, which obstructs ordering in a
+meaningful way.
 
-type GTE = GT `Or` EQ
+Note that these operators may be defined by combining 'Ordering's in certain
+ways: for example @'LT' OR 'EQ'@ could be @LTE@, @'LT' OR 'GT'@ could be @NEQ@.
+This is convenient for user intuition, permitting the use of e.g. 'LT' as a
+relational operator directly. However, it complicates type-level work, as now we
+can't restrict relational operators to a given kind, and we have to handle
+non-standard orderings like @'GT' OR 'LT'@.
+-}
+data RelOp
+  = RelOpEQ  -- ^ @==@              equal to
+  | RelOpNEQ -- ^ @/=@ less than             or greater than (also not equal to)
+  | RelOpLT  -- ^ @<@  less than
+  | RelOpLTE -- ^ @<=@ less than or equal to
+  | RelOpGTE -- ^ @>=@              equal to or greater than
+  | RelOpGT  -- ^ @>@                           greater than
 
--- | Reify a relational operator type tag.
---
--- Permitted operators are @Ordering@ constructors 'LT', 'EQ' and 'GT'; and
--- combinations of these using 'Or'.
-class ReifyRelOp op where
+-- | Reify a 'RelOp'.
+class ReifyRelOp (op :: RelOp) where
     -- | Pretty @op@.
     type ShowRelOp op :: Symbol
 
-    -- | The term-level relational operator that @op@ describes.
+    -- | The term-level relational operator that @op :: 'RelOp'@ describes.
     reifyRelOp :: forall a. Ord a => a -> a -> Bool
 
-instance ReifyRelOp LT where
-    type ShowRelOp LT = "<"
+instance ReifyRelOp RelOpLT  where
+    type ShowRelOp RelOpLT  = "<"
     reifyRelOp = (<)
 
-instance ReifyRelOp LTE where
-    type  ShowRelOp LTE = "<="
+instance ReifyRelOp RelOpLTE where
+    type ShowRelOp RelOpLTE = "<="
     reifyRelOp = (<=)
 
--- | Hidden instance. You won't see this if you use the type synonyms.
-deriving via LTE instance ReifyRelOp (EQ `Or` LT)
-
-instance ReifyRelOp EQ where
-    type  ShowRelOp EQ = "=="
+instance ReifyRelOp RelOpEQ  where
+    type ShowRelOp RelOpEQ  = "=="
     reifyRelOp = (==)
 
-instance ReifyRelOp NEQ where
-    type  ShowRelOp NEQ = "/="
+instance ReifyRelOp RelOpNEQ where
+    type ShowRelOp RelOpNEQ = "/="
     reifyRelOp = (/=)
 
--- | Hidden instance. You won't see this if you use the type synonyms.
-deriving via NEQ instance ReifyRelOp (GT `Or` LT)
-
-instance ReifyRelOp GTE where
-    type ShowRelOp GTE = ">="
+instance ReifyRelOp RelOpGTE where
+    type ShowRelOp RelOpGTE = ">="
     reifyRelOp = (>=)
 
--- | Hidden instance. You won't see this if you use the type synonyms.
-deriving via GTE instance ReifyRelOp (EQ `Or` GT)
-
-instance ReifyRelOp GT where
-    type ShowRelOp GT = ">"
+instance ReifyRelOp RelOpGT  where
+    type ShowRelOp RelOpGT  = ">"
     reifyRelOp = (>)
 
 -- | Can we widen the given 'RelOp' on the given 'Natural' from @n@ to @m@?
-type WidenRelOp :: k -> Natural -> Natural -> Bool
+type WidenRelOp :: RelOp -> Natural -> Natural -> Bool
 type family WidenRelOp op n m where
     -- @n == m@? no problem
     WidenRelOp op  n n = True
 
     -- I'd love to simplify this, but 'CmpNat' is opaque.
-    WidenRelOp LT  n m = OrdCond (CmpNat n m) True  True False
-    WidenRelOp LTE n m = OrdCond (CmpNat n m) True  True False
-    WidenRelOp GTE n m = OrdCond (CmpNat n m) False True True
-    WidenRelOp GT  n m = OrdCond (CmpNat n m) False True True
-
-    -- | swapped LTE, lower down in equation list because less common
-    WidenRelOp (EQ `Or` LT) n m =
-        OrdCond (CmpNat n m) True  True False
-
-    -- | swapped GTE, lower down in equation list because less common
-    WidenRelOp (EQ `Or` GT) n m =
-        OrdCond (CmpNat n m) False True True
+    WidenRelOp RelOpLT  n m = OrdCond (CmpNat n m) True  True False
+    WidenRelOp RelOpLTE n m = OrdCond (CmpNat n m) True  True False
+    WidenRelOp RelOpGTE n m = OrdCond (CmpNat n m) False True True
+    WidenRelOp RelOpGT  n m = OrdCond (CmpNat n m) False True True
 
     -- can't widen (==) or (/=)
-    WidenRelOp _   _ _ = False
+    WidenRelOp op n m = False
 
--- this gets clumsier due to kinding clashes (k vs. Ordering)
-type NormalizeOrRelOp :: Type -> Type
-type family NormalizeOrRelOp op where
-    NormalizeOrRelOp (EQ `Or` LT) = LTE
-    NormalizeOrRelOp (GT `Or` LT) = NEQ
-    NormalizeOrRelOp (EQ `Or` GT) = GTE
+-- | Flip a 'RelOp' to give the opposite comparison.
+type FlipRelOp :: RelOp -> RelOp
+type family FlipRelOp op where
+    FlipRelOp RelOpEQ  = RelOpNEQ
+    FlipRelOp RelOpNEQ = RelOpEQ
+    FlipRelOp RelOpLT  = RelOpGTE
+    FlipRelOp RelOpLTE = RelOpGT
+    FlipRelOp RelOpGTE = RelOpLT
+    FlipRelOp RelOpGT  = RelOpLTE
diff --git a/src/Rerefined/Predicate/Relational/Length.hs b/src/Rerefined/Predicate/Relational/Length.hs
--- a/src/Rerefined/Predicate/Relational/Length.hs
+++ b/src/Rerefined/Predicate/Relational/Length.hs
@@ -17,7 +17,7 @@
 import Data.Text.Builder.Linear qualified as TBL
 
 -- | Compare length to a type-level 'Natural' using the given 'RelOp'.
-data CompareLength op (n :: Natural)
+data CompareLength (op :: RelOp) (n :: Natural)
 
 -- | Precedence of 4 (matching base relational operators e.g. '>=').
 instance Predicate (CompareLength op n) where
diff --git a/src/Rerefined/Predicate/Relational/Value.hs b/src/Rerefined/Predicate/Relational/Value.hs
--- a/src/Rerefined/Predicate/Relational/Value.hs
+++ b/src/Rerefined/Predicate/Relational/Value.hs
@@ -12,7 +12,7 @@
 import GHC.TypeLits ( Symbol )
 
 -- | Compare value to a type-level 'Natural' using the given 'RelOp'.
-data CompareValue op (sign :: Sign) (n :: Natural)
+data CompareValue (op :: RelOp) (sign :: Sign) (n :: Natural)
 
 -- | Precedence of 4 (matching base relational operators e.g. '>=').
 instance Predicate (CompareValue op sign n) where
diff --git a/src/Rerefined/Predicates.hs b/src/Rerefined/Predicates.hs
--- a/src/Rerefined/Predicates.hs
+++ b/src/Rerefined/Predicates.hs
@@ -11,10 +11,10 @@
   , And, Iff, If, Nand, Nor, Not, Or, Xor
 
   -- * Relational
+  , RelOp(..)
   , CompareValue
   , Sign(..)
   , CompareLength
-  , LTE, GTE
   ) where
 
 import Rerefined.Predicate.Succeed
diff --git a/src/Rerefined/Predicates/Operators.hs b/src/Rerefined/Predicates/Operators.hs
--- a/src/Rerefined/Predicates/Operators.hs
+++ b/src/Rerefined/Predicates/Operators.hs
@@ -59,9 +59,9 @@
 type (.->) = If
 
 infix 4 .<, .<=, .==, ./=, .>=, .>
-type (.<)  = LT
-type (.<=) = LTE
-type (.==) =  EQ
-type (./=) = NEQ
-type (.>=) = GTE
-type (.>)  = GT
+type (.<)  = RelOpLT
+type (.<=) = RelOpLTE
+type (.==) = RelOpEQ
+type (./=) = RelOpNEQ
+type (.>=) = RelOpGTE
+type (.>)  = RelOpGT
diff --git a/src/Rerefined/Simplify.hs b/src/Rerefined/Simplify.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Simplify.hs
@@ -0,0 +1,277 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+{- | Primitive predicate simplifier.
+
+This is related to an NP-complete problem (see Boolean satisfiability problem).
+We focus on /immediate, operation-reducing simplifications/, and hope that the
+input is formed in such a way that our rules match.
+
+In short, the simplifier is largely contextless. It inspects (usually) a single
+layer/depth at a time. So we can consistently simplify things like logical
+identities. But don't expect simplifications hard to spot with the naked eye.
+
+The simplifier may not be expectected to consistently implement any
+transformations whatsoever. The only guarantees are
+
+* the output has the same or fewer operations
+* the output meaning is identical to the input
+
+Implementation pitfalls:
+
+* not extensible: only works for built-in logical & relational predicates
+* no protection against non-termination e.g. if a pair of transformations loop
+* very tedious to write. that's life
+-}
+
+module Rerefined.Simplify
+  ( Simplify
+  , SimplifyStep
+  ) where
+
+import Rerefined.Predicate.Succeed
+import Rerefined.Predicate.Fail
+
+import Rerefined.Predicate.Logical
+
+import Rerefined.Predicate.Relational ( CompareLength, CompareValue, FlipRelOp )
+import Rerefined.Simplify.Relational
+  ( SimplifyCompareLength
+  , SimplifyCompareLengthAnd
+  , SimplifyCompareLengthOr
+  )
+
+import Data.Kind ( Type )
+
+-- note that we can't modularize logical simplifications because they're
+-- mutually recursive with the main simplifier :(
+
+-- | Simplify the given predicate.
+--
+-- Returns the input predicate if we were unable to simplify.
+type Simplify :: Type -> Type
+type Simplify p = Simplify' p
+
+-- | Helper definition for reducing duplication.
+type Simplify' p = SimplifyLoop p (SimplifyStep p)
+
+-- | Simplification loop.
+type family SimplifyLoop p mp where
+    -- simplification step succeeded: try again on the simplified predicate
+    SimplifyLoop p (Just p') = Simplify' p'
+
+    -- failed to simplify: give up, return the latest predicate
+    SimplifyLoop p Nothing   = p
+
+-- | Try to perform a single simplification step on the given predicate.
+--
+-- Returns 'Nothing' if we were unable to simplify.
+type family SimplifyStep p where
+    SimplifyStep (Not  p)   = SimplifyNot  p
+
+    SimplifyStep (And  l r) = SimplifyAnd  l r
+    SimplifyStep (Or   l r) = SimplifyOr   l r
+    SimplifyStep (Nand l r) = SimplifyNand l r
+    SimplifyStep (Nor  l r) = SimplifyNor  l r
+    SimplifyStep (Iff  l r) = SimplifyIff  l r
+    SimplifyStep (Xor  l r) = SimplifyXor  l r
+    SimplifyStep (If   l r) = SimplifyIf   l r
+
+    SimplifyStep (CompareLength op n) = SimplifyCompareLength op n
+    -- Don't think we can do anything for CompareValue.
+
+    SimplifyStep p = Nothing
+
+type family SimplifyAnd l r where
+    -- identity laws
+    SimplifyAnd p       Fail    = Just Fail
+    SimplifyAnd Fail    p       = Just Fail
+    SimplifyAnd p       Succeed = Just p
+    SimplifyAnd Succeed p       = Just p
+
+    SimplifyAnd p p = Just p
+
+    -- distributivity
+    SimplifyAnd (Or x y) (Or x z) = Just (Or x (And y z))
+
+    -- special
+    SimplifyAnd (CompareLength lop ln) (CompareLength rop rn) =
+        SimplifyCompareLengthAnd lop ln rop rn
+
+    -- recurse
+    SimplifyAnd l r =
+        (OrElseAndL r (SimplifyStep l)
+            (OrElseAndR l (SimplifyStep r)
+                Nothing))
+
+type family OrElseAndL r mp cont where
+    OrElseAndL r Nothing   cont = cont
+    OrElseAndL r (Just l') cont = Just (And l' r)
+
+type family OrElseAndR l mp cont where
+    OrElseAndR l Nothing   cont = cont
+    OrElseAndR l (Just r') cont = Just (And l r')
+
+type family SimplifyOr l r where
+    -- identity laws
+    SimplifyOr Succeed p       = Just Succeed
+    SimplifyOr p       Succeed = Just Succeed
+    SimplifyOr Fail    p       = Just p
+    SimplifyOr p       Fail    = Just p
+
+    SimplifyOr p p = Just p
+
+    -- distributivity
+    SimplifyOr (And x y) (And x z) = Just (And x (Or y z))
+
+    -- special relational
+    SimplifyOr (CompareLength lop ln) (CompareLength rop rn) =
+        SimplifyCompareLengthOr lop ln rop rn
+
+    -- recurse
+    SimplifyOr l r =
+        (OrElseOrL r (SimplifyStep l)
+            (OrElseOrR l (SimplifyStep r)
+                Nothing))
+
+type family OrElseOrL r mp cont where
+    OrElseOrL r Nothing   cont = cont
+    OrElseOrL r (Just l') cont = Just (Or l' r)
+
+type family OrElseOrR l mp cont where
+    OrElseOrR l Nothing   cont = cont
+    OrElseOrR l (Just r') cont = Just (Or l r')
+
+type family SimplifyNand l r where
+    -- identity laws
+    SimplifyNand Fail    p       = Just Succeed
+    SimplifyNand p       Fail    = Just Succeed
+    SimplifyNand Succeed p       = Just (Not p)
+    SimplifyNand p       Succeed = Just (Not p)
+
+    SimplifyNand p p = Just (Not p)
+
+    -- recurse
+    SimplifyNand l r =
+        (OrElseNandL r (SimplifyStep l)
+            (OrElseNandR l (SimplifyStep r)
+                Nothing))
+
+type family OrElseNandL r mp cont where
+    OrElseNandL r Nothing   cont = cont
+    OrElseNandL r (Just l') cont = Just (Nand l' r)
+
+type family OrElseNandR l mp cont where
+    OrElseNandR l Nothing   cont = cont
+    OrElseNandR l (Just r') cont = Just (Nand l r')
+
+type family SimplifyNor l r where
+    -- identity laws
+    SimplifyNor Succeed p       = Just Fail
+    SimplifyNor p       Succeed = Just Fail
+    SimplifyNor Fail    p       = Just (Not p)
+    SimplifyNor p       Fail    = Just (Not p)
+
+    SimplifyNor p p = Just (Not p)
+
+    -- recurse
+    SimplifyNor l r =
+        (OrElseNorL r (SimplifyStep l)
+            (OrElseNorR l (SimplifyStep r)
+                Nothing))
+
+type family OrElseNorL r mp cont where
+    OrElseNorL r Nothing   cont = cont
+    OrElseNorL r (Just l') cont = Just (Nor l' r)
+
+type family OrElseNorR l mp cont where
+    OrElseNorR l Nothing   cont = cont
+    OrElseNorR l (Just r') cont = Just (Nor l r')
+
+type family SimplifyXor l r where
+    -- identity laws
+    SimplifyXor Fail    p       = Just p
+    SimplifyXor p       Fail    = Just p
+    SimplifyXor Succeed p       = Just (Not p)
+    SimplifyXor p       Succeed = Just (Not p)
+
+    SimplifyXor p p = Just Fail
+
+    -- recurse
+    SimplifyXor l r =
+        (OrElseXorL r (SimplifyStep l)
+            (OrElseXorR l (SimplifyStep r)
+                Nothing))
+
+type family OrElseXorL r mp cont where
+    OrElseXorL r Nothing   cont = cont
+    OrElseXorL r (Just l') cont = Just (Xor l' r)
+
+type family OrElseXorR l mp cont where
+    OrElseXorR l Nothing   cont = cont
+    OrElseXorR l (Just r') cont = Just (Xor l r')
+
+type family SimplifyIf l r where
+    -- identity laws
+    SimplifyIf Fail    p       = Just Succeed
+    SimplifyIf p       Fail    = Just Succeed
+    SimplifyIf Succeed p       = Just p
+    SimplifyIf p       Succeed = Just p
+
+    SimplifyIf p p = Just Succeed
+
+    -- recurse
+    SimplifyIf l r =
+        (OrElseIfL r (SimplifyStep l)
+            (OrElseIfR l (SimplifyStep r)
+                Nothing))
+
+type family OrElseIfL r mp cont where
+    OrElseIfL r Nothing   cont = cont
+    OrElseIfL r (Just l') cont = Just (If l' r)
+
+type family OrElseIfR l mp cont where
+    OrElseIfR l Nothing   cont = cont
+    OrElseIfR l (Just r') cont = Just (If l r')
+
+type family SimplifyIff l r where
+    -- identity laws
+    SimplifyIff Succeed p       = Just p
+    SimplifyIff p       Succeed = Just p
+    SimplifyIff Fail    p       = Just (Not p)
+    SimplifyIff p       Fail    = Just (Not p)
+
+    SimplifyIff p p = Just Succeed
+
+    -- recurse
+    SimplifyIff l r =
+        (OrElseIffL r (SimplifyStep l)
+            (OrElseIffR l (SimplifyStep r)
+                Nothing))
+
+type family OrElseIffL r mp cont where
+    OrElseIffL r Nothing   cont = cont
+    OrElseIffL r (Just l') cont = Just (Iff l' r)
+
+type family OrElseIffR l mp cont where
+    OrElseIffR l Nothing   cont = cont
+    OrElseIffR l (Just r') cont = Just (Iff l r')
+
+type family SimplifyNot p where
+    -- double negation
+    SimplifyNot (Not p) = Just p
+
+    SimplifyNot Succeed = Just Fail
+    SimplifyNot Fail    = Just Succeed
+
+    -- special relational
+    SimplifyNot (CompareLength op      n) =
+        Just (CompareLength (FlipRelOp op)      n)
+    SimplifyNot (CompareValue  op sign n) =
+        Just (CompareValue  (FlipRelOp op) sign n)
+
+    -- recurse
+    SimplifyNot p = OrElseNot (SimplifyStep p) Nothing
+
+type family OrElseNot mp cont where
+    OrElseNot (Just p') cont = Just (Not p')
+    OrElseNot Nothing   cont = cont
diff --git a/src/Rerefined/Simplify/Relational.hs b/src/Rerefined/Simplify/Relational.hs
new file mode 100644
--- /dev/null
+++ b/src/Rerefined/Simplify/Relational.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Rerefined.Simplify.Relational where
+
+import Rerefined.Predicate.Succeed
+import Rerefined.Predicate.Fail
+
+import Rerefined.Predicate.Relational
+import GHC.TypeNats ( Natural, CmpNat )
+import Data.Type.Ord ( OrdCond )
+
+type family SimplifyCompareLength (op :: RelOp) (n :: Natural) where
+    SimplifyCompareLength RelOpLT  0 = Just Fail
+    SimplifyCompareLength RelOpLTE 0 = Just (CompareLength RelOpEQ 0)
+    SimplifyCompareLength RelOpGTE 0 = Just Succeed
+    SimplifyCompareLength RelOpGT  0 = Just (CompareLength RelOpEQ 0)
+
+    SimplifyCompareLength op n = Nothing
+
+type family SimplifyCompareLengthAnd
+  (lop :: RelOp) (ln :: Natural) (rop :: RelOp) (rn :: Natural) where
+    -- @<n AND >m@: @n<=m@ -> False
+    SimplifyCompareLengthAnd RelOpLT  n RelOpGT  m =
+        OrdCond (CmpNat n m)
+            (Just Fail)
+            (Just Fail)
+            Nothing
+    SimplifyCompareLengthAnd RelOpGT  m RelOpLT  n =
+        OrdCond (CmpNat n m)
+            (Just Fail)
+            (Just Fail)
+            Nothing
+
+    SimplifyCompareLengthAnd lop ln rop rn = Nothing
+
+type family SimplifyCompareLengthOr
+  (lop :: RelOp) (ln :: Natural) (rop :: RelOp) (rn :: Natural) where
+    -- @<n OR  >m@: @n==m@ -> NEQ; @n>m@ -> True (?)
+    SimplifyCompareLengthOr RelOpLT  n RelOpGT  m =
+        OrdCond (CmpNat n m)
+            Nothing
+            (Just (CompareLength RelOpNEQ n))
+            (Just Succeed)
+    SimplifyCompareLengthOr RelOpGT  m RelOpLT  n =
+        OrdCond (CmpNat n m)
+            Nothing
+            (Just (CompareLength RelOpNEQ n))
+            (Just Succeed)
+
+    SimplifyCompareLengthOr lop ln rop rn = Nothing