diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index 4e3be387f473c43f990dd7009842f3e97ac71662..a69deb6fb94e4e1104ef575cbeae648cc5416ebe 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -72,6 +72,10 @@ object ListWithSize {
       case Cons(x,xs) => sizeAppend(xs, l2)
     }) ensuring(res => res && size(append(l1,l2)) == size(l1) + size(l2))
 
+    @induct
+    def sizeAppendInductive(l1 : List, l2 : List) : Boolean =
+      (size(append(l1, l2)) == size(l1) + size(l2)) holds
+
     // proved with unrolling=4
     def concat(l1: List, l2: List) : List = concat0(l1, l2, Nil()) 
      // ensuring(content(_) == content(l1) ++ content(l2))