Missing import statement in documentation example

[nunomota]

In the Induction section of Proving Theorems, the below example does not make a reference to leon.proof:

import leon.collection._ // for List
import leon.lang._       // for holds

object Example {
  def reverseReverse[T](l: List[T]): Boolean = {
    l.reverse.reverse == l
  }.holds
}

Which is then needed in the following steps (for because, check and trivial calls):

def reverseReverse[T](l: List[T]): Boolean = {
  l.reverse.reverse == l because {
    l match {
      case Nil()       => check {  Nil[T]().reverse.reverse == Nil[T]()  }
      case Cons(x, xs) => check { (x :: xs).reverse.reverse == (x :: xs) }
    }
  }
}.holds

def reverseReverse[T](l: List[T]): Boolean = {
  l.reverse.reverse == l because {
    l match {
      case Nil()       => trivial
      case Cons(x, xs) => check { (xs.reverse :+ x).reverse == (x :: xs) }
    }
  }
}.holds

[manoskouk]

@mantognini Maybe you want to look into this?

[mantognini]

While because and check were already introduced before, we could add import leon.proof._ // for check, trivial and because as well to make things more obvious and simplify copy-pasting the examples. It would also be a bit more consistent with other snippets.