import stainless.annotation._
import stainless.collection._

object PreInPre {
  @induct
  def f(t: List[BigInt], st: BigInt) {
    require(t.head == st)
  }
}

import stainless.annotation._
import stainless.collection._

object PreInPre {

  @induct
  def f(t: List[BigInt], st: BigInt): Unit = {
    require(t.head == st)
    ()
  }

}

Fix silent extraction issue with Dotty
Fix silent extraction issue with Dotty
