1 files changed, 3 insertions, 6 deletions
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 835c3043..4aaa9a38 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -204,7 +204,7 @@ function insort(n: Nat, xs: List): List
   case Cons(y, ys) =>
     if leq(n, y) == True
     then Cons(n, Cons(y, ys))
-    else Cons(y, ins(n, ys))
+    else Cons(y, insort(n, ys))
 }
 
 function ins(n: Nat, xs: List): List
@@ -397,11 +397,8 @@ ghost method P19()
 ghost method P20()
   ensures forall xs :: len(sort(xs)) == len(xs);
 {
-  P15();  // use the statement of problem 15 as a lemma
-  // ... and manually introduce a case distinction:
-  assert forall ys ::
-           sort(ys) == Nil ||
-           exists z, zs :: sort(ys) == Cons(z, zs);
+  // the proof of this theorem requires a lemma about "insort"
+  assert forall x, xs :: len(insort(x, xs)) == Suc(len(xs));
 }
 
 ghost method P21()