diff --git a/docs/source/typedd/typedd.rst b/docs/source/typedd/typedd.rst
index 287cc1a50d..89a40ef99c 100644
--- a/docs/source/typedd/typedd.rst
+++ b/docs/source/typedd/typedd.rst
@@ -281,28 +281,35 @@ in the type:
 .. code-block:: idris
 
     snocListHelp : {input : _} ->
-                   (snoc : SnocList input) -> (rest : List a) -> SnocList (input +
+                   (snoc : SnocList input) -> (rest : List a) -> SnocList (input ++ rest)
 
 It's no longer necessary to give ``{input}`` explicitly in the patterns for
 ``snocListHelp``, although it's harmless to do so.
 
-In ``IsSuffix.idr``, the matching has to be written slightly differently. The
-recursive with application in Idris 1 probably shouldn't have allowed this!
-Note that the ``Snoc`` - ``Snoc`` case has to be written first otherwise Idris
-generates a case tree splitting on ``input1`` and ``input2`` instead of the
-``SnocList`` objects and this leads to a lot of cases being detected as missing.
+``IsSuffix.idr`` also has to be adjusted to match the new ``Snoc`` arguments.
 
 .. code-block:: idris
 
+  total
   isSuffix : Eq a => List a -> List a -> Bool
-  isSuffix input1 input2 with (snocList input1, snocList input2)
-    isSuffix _ _ | (Snoc x xs xsrec, Snoc y ys ysrec)
-       = (x == y) && (isSuffix _ _ | (xsrec, ysrec))
-    isSuffix _ _ | (Empty, s) = True
-    isSuffix _ _ | (s, Empty) = False
-
-This doesn't yet get past the totality checker, however, because it doesn't
-know about looking inside pairs.
+  isSuffix input1 input2 with (snocList input1)
+    isSuffix [] input2 | Empty = True
+    isSuffix (xs ++ [x]) input2 | (Snoc x xs xsrec) with (snocList input2)
+      isSuffix (xs ++ [x]) [] | (Snoc x xs xsrec) | Empty = False
+      isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc x xs xsrec) | (Snoc y ys ysrec)
+        = if x == y then isSuffix xs ys | xsrec else False
+
+For the ``SplitRec`` view in the exercise 2 after Chapter 10-2 ``import Data.Vect.Views.Extra``
+from ``contrib`` library. The ``n`` argument needs to be made explicit, and so
+does the ``xs`` and ``ys`` for the ``SplitRecPair`` constructor.
+
+.. code-block:: idris
+
+   mergeSort : {n : _} -> Ord a => Vect n a -> Vect n a
+   mergeSort xs with (splitRec xs)
+     mergeSort [] | SplitRecNil = ?mergeSort_rhs_rhss_0
+     mergeSort [x] | SplitRecOne = ?mergeSort_rhs_rhss_1
+     mergeSort (xs ++ ys) | (SplitRecPair {xs} {ys} lrec rrec) = ?mergeSort_rhs_rhss_2
 
 For the ``VList`` view in the exercise 4 after Chapter 10-2 ``import Data.List.Views.Extra`` from ``contrib`` library.
 
diff --git a/tests/typedd-book/chapter10/IsSuffix.idr b/tests/typedd-book/chapter10/IsSuffix.idr
index 4c50e8d6e6..77c6ddf98b 100644
--- a/tests/typedd-book/chapter10/IsSuffix.idr
+++ b/tests/typedd-book/chapter10/IsSuffix.idr
@@ -1,9 +1,10 @@
 import Data.List.Views
 
--- total
+total
 isSuffix : Eq a => List a -> List a -> Bool
-isSuffix input1 input2 with (snocList input1, snocList input2)
-  isSuffix _ _ | (Snoc x xs xsrec, Snoc y ys ysrec)
-     = (x == y) && (isSuffix _ _ | (xsrec, ysrec))
-  isSuffix _ _ | (Empty, s) = True
-  isSuffix _ _ | (s, Empty) = False
+isSuffix input1 input2 with (snocList input1)
+  isSuffix [] input2 | Empty = True
+  isSuffix (xs ++ [x]) input2 | (Snoc x xs xsrec) with (snocList input2)
+    isSuffix (xs ++ [x]) [] | (Snoc x xs xsrec) | Empty = False
+    isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc x xs xsrec) | (Snoc y ys ysrec)
+      = if x == y then isSuffix xs ys | xsrec else False