diff --git a/library/collection/List.scala b/library/collection/List.scala
index 60a5f25ec44aa9487cf96fa74af69b3b514d9e35..f8d3fb333601723960f62e851e815e306e867c68 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -223,7 +223,7 @@ sealed abstract class List[T] {
           case Some(i) => Some(i+1)
         }
       }
-  }} ensuring { _.isDefined == this.contains(e) }
+    }} ensuring { res => !res.isDefined || (this.content contains e) }
 
   def init: List[T] = {
     require(!isEmpty)
@@ -410,7 +410,7 @@ sealed abstract class List[T] {
     case Nil() => None[T]()
     case Cons(h, t) if p(h) => Some(h)
     case Cons(_, t) => t.find(p)
-  }} ensuring { _.isDefined == exists(p) }
+  }} ensuring { res => !res.isDefined || content.contains(res.get) }
 
   def groupBy[R](f: T => R): Map[R, List[T]] = this match {
     case Nil() => Map.empty[R, List[T]]
diff --git a/library/collection/Option.scala b/library/collection/Option.scala
index 769008e4fea2838995677f8b48d5b8aa332c4050..56feffdc0fc5b017b8b8a5dc9862d1f3a06d5811 100644
--- a/library/collection/Option.scala
+++ b/library/collection/Option.scala
@@ -19,9 +19,11 @@ sealed abstract class Option[T] {
     case None()  => default
   }
 
-  def orElse(or: Option[T]) = this match {
+  def orElse(or: Option[T]) = {this match {
     case Some(v) => this
     case None() => or
+  }} ensuring {
+    res => (this.isDefined || or.isDefined) == res.isDefined
   }
 
   def isEmpty = this match {