Add let case in ChooseEncoder

Created by: jad-hamza

Fix an issue that appeared on this Stainless program, where ChooseEncoder generates a choose function with an unbound variable.

iimport stainless.lang._
import stainless.lang.StaticChecks.WhileDecorations

object Bug {
  def insert[T](array: Array[T]): Unit = {
    val n: Int = array.length
    var i = n - 1

    (while (true) {
      i += 1

    }).inline.opaque.invariant (
      i <= n-1
    )
  }
}