diff --git a/CHANGES.md b/CHANGES.md
index d93e7940a..97b07ca75 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -9,6 +9,8 @@
     by the same name: https://github.com/philzook58/knuckledragger.
 
   * Added several KnuckleDragger proof examples, see Documentation.SBV.Examples.KnuckleDragger modules.
+    Amongst the proofs are the irrationality of square-root of 2, several list lemmas, and a few
+    inductive proofs over naturals.
 
   * Add sDivides, which takes a concrete integer and a (possibly symbolic), and returns sTrue
     if the first argument divides the second. It is essentially equivalent to @a `sMod` n .== 0`,
diff --git a/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs b/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs
new file mode 100644
index 000000000..666fd79fb
--- /dev/null
+++ b/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs
@@ -0,0 +1,42 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module    : Documentation.SBV.Examples.KnuckleDragger.RevLen
+-- Copyright : (c) Levent Erkok
+-- License   : BSD3
+-- Maintainer: erkokl@gmail.com
+-- Stability : experimental
+--
+-- Proof that reversing a list does not change its length.
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeAbstractions    #-}
+
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Documentation.SBV.Examples.KnuckleDragger.RevLen where
+
+import Prelude hiding (length, reverse)
+
+import Data.SBV
+import Data.SBV.Tools.KnuckleDragger
+
+import Data.SBV.List (reverse, length)
+
+-- | @length xs == length (reverse xs)@
+--
+-- We have:
+--
+-- >>> revLen
+-- Lemma: revLen                           Q.E.D.
+revLen :: IO Proven
+revLen = do
+   let p :: SList Integer -> SBool
+       p xs = length (reverse xs) .== length xs
+
+   induct <- inductionPrinciple p
+
+   lemma "revLen"
+         (\(Forall @"xs" xs) -> p xs)
+         [induct]
diff --git a/sbv.cabal b/sbv.cabal
index 1fd6eecec..c77cf6999 100644
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -156,6 +156,7 @@ Library
                   , Documentation.SBV.Examples.KnuckleDragger.Kleene
                   , Documentation.SBV.Examples.KnuckleDragger.Induction
                   , Documentation.SBV.Examples.KnuckleDragger.ListLen
+                  , Documentation.SBV.Examples.KnuckleDragger.RevLen
                   , Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational
                   , Documentation.SBV.Examples.Misc.Definitions
                   , Documentation.SBV.Examples.Misc.Enumerate