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

object PreInPre {

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

}

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

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

--- 
+++ 
@@ -2,8 +2,11 @@
 import stainless.collection._
 
 object PreInPre {
+
   @induct
-  def f(t: List[BigInt], st: BigInt) {
+  def f(t: List[BigInt], st: BigInt): Unit = {
     require(t.head == st)
+    ()
   }
+
 }
Fix silent extraction issue with Dotty
