diff --git a/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs b/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs
index 50448cc17..170c5ad89 100644
--- a/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs
@@ -47,7 +47,7 @@ consApp = lemma "consApp"
              (\(Forall @"x" (x :: SInteger)) (Forall @"xs" xs) (Forall @"ys" ys) -> (x .: xs) ++ ys .== x .: (xs ++ ys))
              []
 
--- | Prove that list append is associative.
+-- | @(xs ++ ys) ++ zs == xs ++ (ys ++ zs)@
 --
 -- We have:
 -- >>> appendAssoc