diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index ad7ae73770ba92ccb9ce2a9662a759f713c6d43f..3e4af03bd526ccf122a6d05f63f4872b9f69688a 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -546,6 +546,7 @@ trait CodeGeneration {
 
       case l @ Lambda(args, body) =>
         val afName = "Leon$CodeGen$Lambda$" + CompilationUnit.nextLambdaId
+        lambdas += afName -> l
 
         val cf = new ClassFile(afName, Some(LambdaClass))
 
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index e183533b5ece0fe30b49ba31fe18c045b0236801..2a9cdce02638d40c844236993d1cd8f20a8b9907 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -28,6 +28,7 @@ class CompilationUnit(val ctx: LeonContext,
 
   val loader = new CafebabeClassLoader(classOf[CompilationUnit].getClassLoader)
 
+  var lambdas     = Map[String, Lambda]()
   var classes     = Map[Definition, ClassFile]()
   var defToModuleOrClass = Map[Definition, Definition]()
   
@@ -229,10 +230,10 @@ class CompilationUnit(val ctx: LeonContext,
       if (gtp == tp) gv
       else GenericValue(tp, id).copiedFrom(gv)
 
-    case (set : runtime.Set, SetType(b)) =>
+    case (set: runtime.Set, SetType(b)) =>
       finiteSet(set.getElements.asScala.map(jvmToExpr(_, b)).toSet, b)
 
-    case (map : runtime.Map, MapType(from, to)) =>
+    case (map: runtime.Map, MapType(from, to)) =>
       val pairs = map.getElements.asScala.map { entry =>
         val k = jvmToExpr(entry.getKey, from)
         val v = jvmToExpr(entry.getValue, to)
@@ -240,6 +241,18 @@ class CompilationUnit(val ctx: LeonContext,
       }
       finiteMap(pairs.toSeq, from, to)
 
+    case (lambda: runtime.Lambda, _: FunctionType) =>
+      val cls = lambda.getClass
+
+      val l = lambdas(cls.getName)
+      val closures = purescala.ExprOps.variablesOf(l).toSeq.sortBy(_.uniqueName)
+      val closureVals = closures.map { id =>
+        val fieldVal = lambda.getClass.getField(id.name).get(lambda)
+        jvmToExpr(fieldVal, id.getType)
+      }
+
+      purescala.ExprOps.replaceFromIDs((closures zip closureVals).toMap, l)
+
     case (_, UnitType) =>
       UnitLiteral()
 
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 1465cd5325d7ad83cd5e08ef34b607af45f46693..20bd917324e4e481af824aa261162f359c56ed88 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -158,10 +158,9 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
     }
   }
 
-  private def T = BooleanLiteral(true)
-  private def F = BooleanLiteral(false)
-  private def IL(i : Int) = IntLiteral(i)
-  private def BIL(i : Int) = InfiniteIntegerLiteral(i)
+  private val T = BooleanLiteral(true)
+  private val F = BooleanLiteral(false)
+  import purescala.Expressions.{IntLiteral => IL, InfiniteIntegerLiteral => BIL}
 
   test("Arithmetic") {
     val p = """|object Program {
@@ -583,4 +582,40 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
       checkComp(e, mkCall("f6"), IL(1))
     }
   }
+
+  test("Lambda functions") {
+    val p = """import leon.lang._
+              |object Program {
+              |  val foo1 = (x: BigInt) => x
+              |  val foo2 = {
+              |    val a = BigInt(1)
+              |    (x: BigInt) => a + x
+              |  }
+              |  val foo3 = {
+              |    val f1 = (x: BigInt) => x + 1
+              |    val f2 = (x: BigInt) => x + 2
+              |    (x: BigInt, y: BigInt) => f1(x) + f2(y)
+              |  }
+              |  def foo4(x: BigInt) = (i: BigInt) => i + x
+              |}""".stripMargin
+
+    implicit val prog = parseString(p)
+    val evaluators = prepareEvaluators
+
+    def checkLambda(evaluator: Evaluator, in: Expr, out: PartialFunction[Expr, Boolean]) {
+      val result = checkCompSuccess(evaluator, in)
+      if (!out.isDefinedAt(result) || !out(result))
+        throw new AssertionError(s"Evaluation of '$in' with evaluator '${evaluator.name}' produced invalid '$result'.")
+    }
+
+    val ONE = BIL(1)
+    val TWO = BIL(2)
+
+    for(e <- evaluators) {
+      checkLambda(e, mkCall("foo1"), { case Lambda(Seq(vd), Variable(id)) if vd.id == id => true })
+      checkLambda(e, mkCall("foo2"), { case Lambda(Seq(vd), Plus(ONE, Variable(id))) if vd.id == id => true })
+      checkLambda(e, mkCall("foo3"), { case Lambda(Seq(vx, vy), Plus(Plus(Variable(x), ONE), Plus(Variable(y), TWO))) if vx.id == x && vy.id == y => true })
+      checkLambda(e, mkCall("foo4", TWO), { case Lambda(Seq(vd), Plus(Variable(id), TWO)) if vd.id == id => true })
+    }
+  }
 }
diff --git a/testcases/termination/List.scala b/testcases/termination/List.scala
new file mode 100644
index 0000000000000000000000000000000000000000..60a5f25ec44aa9487cf96fa74af69b3b514d9e35
--- /dev/null
+++ b/testcases/termination/List.scala
@@ -0,0 +1,613 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.collection
+
+import leon._
+import leon.lang._
+import leon.annotation._
+import leon.math._
+
+@library
+sealed abstract class List[T] {
+
+  def size: BigInt = (this match {
+    case Nil() => BigInt(0)
+    case Cons(h, t) => 1 + t.size
+  }) ensuring (_ >= 0)
+
+  def content: Set[T] = this match {
+    case Nil() => Set()
+    case Cons(h, t) => Set(h) ++ t.content
+  }
+
+  def contains(v: T): Boolean = (this match {
+    case Cons(h, t) if h == v => true
+    case Cons(_, t) => t.contains(v)
+    case Nil() => false
+  }) ensuring { _ == (content contains v) }
+
+  def ++(that: List[T]): List[T] = (this match {
+    case Nil() => that
+    case Cons(x, xs) => Cons(x, xs ++ that)
+  }) ensuring { res =>
+    (res.content == this.content ++ that.content) && 
+    (res.size == this.size + that.size)
+  }
+
+  def head: T = {
+    require(this != Nil[T]())
+    val Cons(h, _) = this
+    h
+  }
+
+  def tail: List[T] = {
+    require(this != Nil[T]())
+    val Cons(_, t) = this
+    t
+  }
+
+  def apply(index: BigInt): T = {
+    require(0 <= index && index < size)
+    if (index == BigInt(0)) {
+      head
+    } else {
+      tail(index-1)
+    }
+  }
+
+  def ::(t:T): List[T] = Cons(t, this)
+
+  def :+(t:T): List[T] = {
+    this match {
+      case Nil() => Cons(t, this)
+      case Cons(x, xs) => Cons(x, xs :+ (t))
+    }
+  } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
+
+  def reverse: List[T] = {
+    this match {
+      case Nil() => this
+      case Cons(x,xs) => xs.reverse :+ x
+    }
+  } ensuring (res => (res.size == size) && (res.content == content))
+
+  def take(i: BigInt): List[T] = { (this, i) match {
+    case (Nil(), _) => Nil[T]()
+    case (Cons(h, t), i) =>
+      if (i <= BigInt(0)) {
+        Nil[T]()
+      } else {
+        Cons(h, t.take(i-1))
+      }
+  }} ensuring { res =>
+    res.content.subsetOf(this.content) && (res.size == (
+      if      (i <= 0)         BigInt(0)
+      else if (i >= this.size) this.size
+      else                     i
+    ))
+  }
+
+  def drop(i: BigInt): List[T] = { (this, i) match {
+    case (Nil(), _) => Nil[T]()
+    case (Cons(h, t), i) =>
+      if (i <= BigInt(0)) {
+        Cons[T](h, t)
+      } else {
+        t.drop(i-1)
+      }
+  }} ensuring { res =>
+    res.content.subsetOf(this.content) && (res.size == (
+      if      (i <= 0)         this.size
+      else if (i >= this.size) BigInt(0)
+      else                     this.size - i
+    ))
+  }
+
+  def slice(from: BigInt, to: BigInt): List[T] = {
+    require(0 <= from && from <= to && to <= size)
+    drop(from).take(to-from)
+  }
+
+  def replace(from: T, to: T): List[T] = { this match {
+    case Nil() => Nil[T]()
+    case Cons(h, t) =>
+      val r = t.replace(from, to)
+      if (h == from) {
+        Cons(to, r)
+      } else {
+        Cons(h, r)
+      }
+  }} ensuring { (res: List[T]) =>
+    res.size == this.size &&
+    res.content == (
+      (this.content -- Set(from)) ++
+      (if (this.content contains from) Set(to) else Set[T]())
+    )
+  }
+
+  private def chunk0(s: BigInt, l: List[T], acc: List[T], res: List[List[T]], s0: BigInt): List[List[T]] = l match {
+    case Nil() =>
+      if (acc.size > 0) {
+        res :+ acc
+      } else {
+        res
+      }
+    case Cons(h, t) =>
+      if (s0 == BigInt(0)) {
+        chunk0(s, l, Nil(), res :+ acc, s)
+      } else {
+        chunk0(s, t, acc :+ h, res, s0-1)
+      }
+  }
+
+  def chunks(s: BigInt): List[List[T]] = {
+    require(s > 0)
+
+    chunk0(s, this, Nil(), Nil(), s)
+  }
+
+  def zip[B](that: List[B]): List[(T, B)] = { (this, that) match {
+    case (Cons(h1, t1), Cons(h2, t2)) =>
+      Cons((h1, h2), t1.zip(t2))
+    case _ =>
+      Nil[(T, B)]()
+  }} ensuring { _.size == (
+    if (this.size <= that.size) this.size else that.size
+  )}
+
+  def -(e: T): List[T] = { this match {
+    case Cons(h, t) =>
+      if (e == h) {
+        t - e
+      } else {
+        Cons(h, t - e)
+      }
+    case Nil() =>
+      Nil[T]()
+  }} ensuring { res =>
+    res.size <= this.size &&
+    res.content == this.content -- Set(e)
+  }
+
+  def --(that: List[T]): List[T] = { this match {
+    case Cons(h, t) =>
+      if (that.contains(h)) {
+        t -- that
+      } else {
+        Cons(h, t -- that)
+      }
+    case Nil() =>
+      Nil[T]()
+  }} ensuring { res =>
+    res.size <= this.size &&
+    res.content == this.content -- that.content
+  }
+
+  def &(that: List[T]): List[T] = { this match {
+    case Cons(h, t) =>
+      if (that.contains(h)) {
+        Cons(h, t & that)
+      } else {
+        t & that
+      }
+    case Nil() =>
+      Nil[T]()
+  }} ensuring { res =>
+    res.size <= this.size &&
+    res.content == (this.content & that.content)
+  }
+
+  def padTo(s: BigInt, e: T): List[T] = { (this, s) match {
+    case (_, s) if s <= 0 =>
+      this
+    case (Nil(), s) =>
+      Cons(e, Nil().padTo(s-1, e))
+    case (Cons(h, t), s) =>
+      Cons(h, t.padTo(s-1, e))
+  }} ensuring { res =>
+    if (s <= this.size)
+      res == this
+    else
+      res.size == s &&
+      res.content == this.content ++ Set(e)
+  }
+
+  def find(e: T): Option[BigInt] = { this match {
+    case Nil() => None[BigInt]()
+    case Cons(h, t) =>
+      if (h == e) {
+        Some[BigInt](0)
+      } else {
+        t.find(e) match {
+          case None()  => None[BigInt]()
+          case Some(i) => Some(i+1)
+        }
+      }
+  }} ensuring { _.isDefined == this.contains(e) }
+
+  def init: List[T] = {
+    require(!isEmpty)
+    (this match {
+      case Cons(h, Nil()) =>
+        Nil[T]()
+      case Cons(h, t) =>
+        Cons[T](h, t.init)
+    })
+  } ensuring ( (r: List[T]) =>
+    r.size == this.size - 1 &&
+    r.content.subsetOf(this.content)
+  )
+
+  def last: T = {
+    require(!isEmpty)
+    this match {
+      case Cons(h, Nil()) => h
+      case Cons(_, t) => t.last
+    }
+  } ensuring { this.contains _ }
+
+  def lastOption: Option[T] = { this match {
+    case Cons(h, t) =>
+      t.lastOption.orElse(Some(h))
+    case Nil() =>
+      None[T]()
+  }} ensuring { _.isDefined != this.isEmpty }
+
+  def firstOption: Option[T] = { this match {
+    case Cons(h, t) =>
+      Some(h)
+    case Nil() =>
+      None[T]()
+  }} ensuring { _.isDefined != this.isEmpty }
+
+  def unique: List[T] = this match {
+    case Nil() => Nil()
+    case Cons(h, t) =>
+      Cons(h, t.unique - h)
+  }
+
+  def splitAt(e: T): List[List[T]] =  split(Cons(e, Nil()))
+
+  def split(seps: List[T]): List[List[T]] = this match {
+    case Cons(h, t) =>
+      if (seps.contains(h)) {
+        Cons(Nil(), t.split(seps))
+      } else {
+        val r = t.split(seps)
+        Cons(Cons(h, r.head), r.tail)
+      }
+    case Nil() =>
+      Cons(Nil(), Nil())
+  }
+
+  def evenSplit: (List[T], List[T]) = {
+    val c = size/2
+    (take(c), drop(c))
+  }
+
+  def insertAt(pos: BigInt, l: List[T]): List[T] = {
+    if(pos < 0) {
+      insertAt(size + pos, l)
+    } else if(pos == BigInt(0)) {
+      l ++ this
+    } else {
+      this match {
+        case Cons(h, t) =>
+          Cons(h, t.insertAt(pos-1, l))
+        case Nil() =>
+          l
+      }
+    }
+  } ensuring { res =>
+    res.size == this.size + l.size &&
+    res.content == this.content ++ l.content
+  }
+
+  def replaceAt(pos: BigInt, l: List[T]): List[T] = {
+    if(pos < 0) {
+      replaceAt(size + pos, l)
+    } else if(pos == BigInt(0)) {
+      l ++ this.drop(l.size)
+    } else {
+      this match {
+        case Cons(h, t) =>
+          Cons(h, t.replaceAt(pos-1, l))
+        case Nil() =>
+          l
+      }
+    }
+  } ensuring { res =>
+    res.content.subsetOf(l.content ++ this.content)
+  }
+
+  def rotate(s: BigInt): List[T] = {
+    if (s < 0) {
+      rotate(size + s)
+    } else if (s > size) {
+      rotate(s - size)
+    } else {
+      drop(s) ++ take(s)
+    }
+  } ensuring { res =>
+    res.size == this.size
+  }
+
+  def isEmpty = this match { 
+    case Nil() => true
+    case _ => false 
+  }
+
+  // Higher-order API
+  def map[R](f: T => R): List[R] = { this match {
+    case Nil() => Nil[R]()
+    case Cons(h, t) => f(h) :: t.map(f)
+  }} ensuring { _.size == this.size }
+
+  def foldLeft[R](z: R)(f: (R,T) => R): R = this match {
+    case Nil() => z
+    case Cons(h,t) => t.foldLeft(f(z,h))(f)
+  }
+
+  def foldRight[R](z: R)(f: (T,R) => R): R = this match {
+    case Nil() => z
+    case Cons(h, t) => f(h, t.foldRight(z)(f))
+  }
+ 
+  def scanLeft[R](z: R)(f: (R,T) => R): List[R] = { this match {
+    case Nil() => z :: Nil()
+    case Cons(h,t) => z :: t.scanLeft(f(z,h))(f)
+  }} ensuring { !_.isEmpty }
+
+  def scanRight[R](z: R)(f: (T,R) => R): List[R] = { this match {
+    case Nil() => z :: Nil[R]()
+    case Cons(h, t) => 
+      val rest@Cons(h1,_) = t.scanRight(z)(f)
+      f(h, h1) :: rest
+  }} ensuring { !_.isEmpty }
+
+  def flatMap[R](f: T => List[R]): List[R] = 
+    ListOps.flatten(this map f)
+
+  def filter(p: T => Boolean): List[T] = { this match {
+    case Nil() => Nil[T]()
+    case Cons(h, t) if p(h) => Cons(h, t.filter(p))
+    case Cons(_, t) => t.filter(p)
+  }} ensuring { res =>
+    res.size <= this.size &&
+    res.content.subsetOf(this.content) &&
+    res.forall(p)
+  }
+
+  def filterNot(p: T => Boolean): List[T] =
+    filter(!p(_)) ensuring { res =>
+      res.size <= this.size &&
+      res.content.subsetOf(this.content) &&
+      res.forall(!p(_))
+    }
+
+  def partition(p: T => Boolean): (List[T], List[T]) = { this match {
+    case Nil() => (Nil[T](), Nil[T]())
+    case Cons(h, t) =>
+      val (l1, l2) = t.partition(p)
+      if (p(h)) (h :: l1, l2)
+      else      (l1, h :: l2)
+  }} ensuring { res =>
+    res._1 == filter(p) &&
+    res._2 == filterNot(p)
+  }
+
+  // In case we implement for-comprehensions
+  def withFilter(p: T => Boolean) = filter(p)
+
+  def forall(p: T => Boolean): Boolean = this match {
+    case Nil() => true
+    case Cons(h, t) => p(h) && t.forall(p)
+  }
+
+  def exists(p: T => Boolean) = !forall(!p(_))
+
+  def find(p: T => Boolean): Option[T] = { this match {
+    case Nil() => None[T]()
+    case Cons(h, t) if p(h) => Some(h)
+    case Cons(_, t) => t.find(p)
+  }} ensuring { _.isDefined == exists(p) }
+
+  def groupBy[R](f: T => R): Map[R, List[T]] = this match {
+    case Nil() => Map.empty[R, List[T]]
+    case Cons(h, t) =>
+      val key: R = f(h)
+      val rest: Map[R, List[T]] = t.groupBy(f)
+      val prev: List[T] = if (rest isDefinedAt key) rest(key) else Nil[T]()
+      (rest ++ Map((key, h :: prev))) : Map[R, List[T]]
+  }
+
+  def takeWhile(p: T => Boolean): List[T] = { this match {
+    case Cons(h,t) if p(h) => Cons(h, t.takeWhile(p))
+    case _ => Nil[T]()
+  }} ensuring { res =>
+    (res forall p) &&
+    (res.size <= this.size) &&
+    (res.content subsetOf this.content)
+  }
+
+  def dropWhile(p: T => Boolean): List[T] = { this match {
+    case Cons(h,t) if p(h) => t.dropWhile(p)
+    case _ => this
+  }} ensuring { res =>
+    (res.size <= this.size) &&
+    (res.content subsetOf this.content) &&
+    (res.isEmpty || !p(res.head))
+  }
+
+  def count(p: T => Boolean): BigInt = { this match {
+    case Nil() => BigInt(0)
+    case Cons(h, t) =>
+      (if (p(h)) BigInt(1) else BigInt(0)) + t.count(p)
+  }} ensuring {
+    _ == this.filter(p).size
+  }
+
+}
+
+@ignore
+object List {
+  def apply[T](elems: T*): List[T] = {
+    var l: List[T] = Nil[T]()
+    for (e <- elems) {
+      l = Cons(e, l)
+    }
+    l.reverse
+  }
+}
+
+@library
+object ListOps {
+  def flatten[T](ls: List[List[T]]): List[T] = ls match {
+    case Cons(h, t) => h ++ flatten(t)
+    case Nil() => Nil()
+  }
+
+  def isSorted(ls: List[BigInt]): Boolean = ls match {
+    case Nil() => true
+    case Cons(_, Nil()) => true
+    case Cons(h1, Cons(h2, _)) if(h1 > h2) => false
+    case Cons(_, t) => isSorted(t)
+  }
+
+  def sorted(ls: List[BigInt]): List[BigInt] = ls match {
+    case Cons(h, t) => insSort(sorted(t), h)
+    case Nil() => Nil()
+  }
+
+  def insSort(ls: List[BigInt], v: BigInt): List[BigInt] = ls match {
+    case Nil() => Cons(v, Nil())
+    case Cons(h, t) =>
+      if (v <= h) {
+        Cons(v, t)
+      } else {
+        Cons(h, insSort(t, v))
+      }
+  }
+}
+
+case class Cons[T](h: T, t: List[T]) extends List[T]
+case class Nil[T]() extends List[T]
+
+@library
+object ListSpecs {
+  def snocIndex[T](l : List[T], t : T, i : BigInt) : Boolean = {
+    require(0 <= i && i < l.size + 1)
+    // proof:
+    (l match {
+      case Nil() => true
+      case Cons(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
+    }) &&
+    // claim:
+    ((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
+  }.holds
+
+  def reverseIndex[T](l : List[T], i : BigInt) : Boolean = {
+    require(0 <= i && i < l.size)
+    (l match {
+      case Nil() => true
+      case Cons(x,xs) => snocIndex(l, x, i) && reverseIndex[T](l,i)
+    }) &&
+    (l.reverse.apply(i) == l.apply(l.size - 1 - i))
+  }.holds
+
+  def appendIndex[T](l1 : List[T], l2 : List[T], i : BigInt) : Boolean = {
+    require(0 <= i && i < l1.size + l2.size)
+    (l1 match {
+      case Nil() => true
+      case Cons(x,xs) => if (i==BigInt(0)) true else appendIndex[T](xs,l2,i-1)
+    }) &&
+    ((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
+  }.holds
+
+  def appendAssoc[T](l1 : List[T], l2 : List[T], l3 : List[T]) : Boolean = {
+    (l1 match {
+      case Nil() => true
+      case Cons(x,xs) => appendAssoc(xs,l2,l3)
+    }) &&
+    (((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3)))
+  }.holds
+
+  def snocIsAppend[T](l : List[T], t : T) : Boolean = {
+    (l match {
+      case Nil() => true
+      case Cons(x,xs) =>  snocIsAppend(xs,t)
+    }) &&
+    ((l :+ t) == l ++ Cons[T](t, Nil()))
+  }.holds
+
+  def snocAfterAppend[T](l1 : List[T], l2 : List[T], t : T) : Boolean = {
+    (l1 match {
+      case Nil() => true
+      case Cons(x,xs) =>  snocAfterAppend(xs,l2,t)
+    }) &&
+    ((l1 ++ l2) :+ t == (l1 ++ (l2 :+ t)))
+  }.holds
+
+  def snocReverse[T](l : List[T], t : T) : Boolean = {
+    (l match {
+      case Nil() => true
+      case Cons(x,xs) => snocReverse(xs,t)
+    }) &&
+    ((l :+ t).reverse == Cons(t, l.reverse))
+  }.holds
+
+  def reverseReverse[T](l : List[T]) : Boolean = {
+    (l match {
+      case Nil() => true
+      case Cons(x,xs) => reverseReverse[T](xs) && snocReverse[T](xs.reverse, x)
+    }) &&
+    (l.reverse.reverse == l)
+  }.holds
+
+  //// my hand calculation shows this should work, but it does not seem to be found
+  //def reverseAppend[T](l1 : List[T], l2 : List[T]) : Boolean = {
+  //  (l1 match {
+  //    case Nil() => true
+  //    case Cons(x,xs) => {
+  //      reverseAppend(xs,l2) &&
+  //      snocAfterAppend[T](l2.reverse, xs.reverse, x) &&
+  //      l1.reverse == (xs.reverse :+ x)
+  //    }
+  //  }) &&
+  //  ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
+  //}.holds
+
+  //def associative[T,U](l1: List[T], l2: List[T], f: List[T] => U, op: (U,U) => U) = {
+  //  f(l1 ++ l2) == op(f(l1), f(l2))
+  //}
+  //
+  //def existsAssoc[T](l1: List[T], l2: List[T], p: T => Boolean) = {
+  //  associative[T, Boolean](l1, l2, _.exists(p), _ || _ )
+  //}.holds
+  //
+  //def forallAssoc[T](l1: List[T], l2: List[T], p: T => Boolean) = {
+  //  associative[T, Boolean](l1, l2, _.exists(p), _ && _ )
+  //}.holds
+
+  //@induct
+  //def folds[T,R](l : List[T], z : R, f : (R,T) => R) = {
+  //  { l match {
+  //    case Nil() => true
+  //    case Cons(h,t) => snocReverse[T](t, h)
+  //  }} &&
+  //  l.foldLeft(z)(f) == l.reverse.foldRight((x:T,y:R) => f(y,x))(z)
+  //}.holds
+  //
+
+  //Can't prove this
+  //@induct
+  //def scanVsFoldLeft[A,B](l : List[A], z: B, f: (B,A) => B): Boolean = {
+  //  l.scanLeft(z)(f).last == l.foldLeft(z)(f)
+  //}.holds
+
+  @induct
+  def scanVsFoldRight[A,B](l: List[A], z: B, f: (A,B) => B): Boolean = {
+    l.scanRight(z)(f).head == l.foldRight(z)(f)
+  }.holds
+
+}