diff --git a/Documentation/SBV/Examples/KnuckleDragger/Lists.hs b/Documentation/SBV/Examples/KnuckleDragger/Lists.hs
index 270bf66a..c6554647 100644
--- a/Documentation/SBV/Examples/KnuckleDragger/Lists.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/Lists.hs
@@ -79,10 +79,6 @@ mkUninterpretedSort ''A
 data B
 mkUninterpretedSort ''B
 
--- | An uninterpreted function, for use as a witness in the following higher-order proofs.
-f :: SA -> SB
-f = uninterpret "f"
-
 -- | @reverse (x:xs) == reverse xs ++ [x]@
 --
 -- >>> runKD revCons
@@ -105,6 +101,10 @@ mapAppend = do
    let p :: (SA -> SB) -> SList A -> SList A -> SBool
        p g xs ys = map g (xs ++ ys) .== map g xs ++ map g ys
 
+       -- For an arbitrary uninterpreted function 'f':
+       f :: SA -> SB
+       f = uninterpret "f"
+
    lemma "mapAppend"
          (\(Forall @"xs" xs) (Forall @"ys" ys) -> p f xs ys)
          -- induction is done on the last argument, so flip to do it on xs
@@ -129,6 +129,10 @@ mapReverse = do
      let p :: (SA -> SB) -> SList A -> SBool
          p g xs = reverse (map g xs) .== map g (reverse xs)
 
+         -- For an arbitrary uninterpreted function 'f':
+         f :: SA -> SB
+         f = uninterpret "f"
+
      rCons <- revCons
      mApp  <- mapAppend