diff --git a/testcases/verification/compilation/ExprCompiler.scala b/testcases/verification/compilation/ExprCompiler.scala
index 7518c21fb8ba7349e49c37c8acac6f99aaae2cdd..d6b7d74caa52a4a49255e71781c86f1052c439db 100644
--- a/testcases/verification/compilation/ExprCompiler.scala
+++ b/testcases/verification/compilation/ExprCompiler.scala
@@ -17,22 +17,22 @@ object TinyCertifiedCompiler {
   def compile[A](e: ExprTree[A]): List[ByteCode[A]] = {
     e match {
       case Const(c) =>
-        Cons(Load(c), Nil[ByteCode[A]]())
+        Cons(Load(c), Nil())
       case Op(e1, e2) =>
-        (compile(e1) ++ compile(e2)) ++ Cons(OpInst(), Nil[ByteCode[A]]())
+        (compile(e1) ++ compile(e2)) ++ Cons(OpInst(), Nil())
     }
   }
 
-  def op[A](x: A, y: A): A = {
+  def op[A](x: A, y: A): A = { // uninterpreted
     ???[A]
   }
 
   def run[A](bytecode: List[ByteCode[A]], S: List[A]): List[A] = {
     (bytecode, S) match {
       case (Cons(Load(c), tail), _) =>
-        run(tail, Cons[A](c, S)) // adding elements to the head of the stack
+        run(tail, c :: S) // adding elements to the head of the stack
       case (Cons(OpInst(), tail), Cons(x, Cons(y, rest))) =>
-        run(tail, Cons[A](op(y, x), rest))
+        run(tail, op(y, x) :: rest)
       case (Cons(_, tail), _) =>
         run(tail, S)
       case (Nil(), _) => // no bytecode to execute
@@ -43,8 +43,7 @@ object TinyCertifiedCompiler {
   def interpret[A](e: ExprTree[A]): A = {
     e match {
       case Const(c) => c
-      case Op(e1, e2) =>
-        op(interpret(e1), interpret(e2))
+      case Op(e1, e2) => op(interpret(e1), interpret(e2))
     }
   }
 
@@ -53,8 +52,7 @@ object TinyCertifiedCompiler {
     (run(l1 ++ l2, S) == run(l2, run(l1, S))) because
       // induction scheme (induct over l1)
       (l1 match {
-        case Nil() =>
-          true
+        case Nil() => true
         case Cons(h, tail) =>
           (h, S) match {
             case (Load(c), _) =>
@@ -63,8 +61,7 @@ object TinyCertifiedCompiler {
               runAppendLemma(tail, l2, Cons[A](op(y, x), rest))
             case (_, _) =>
               runAppendLemma(tail, l2, S)
-            case _ =>
-              true
+            case _ => true
           }
       })
   }.holds
@@ -74,16 +71,15 @@ object TinyCertifiedCompiler {
     (run(compile(e), S) == interpret(e) :: S) because 
       // induction scheme
       (e match {
-        case Const(c) =>
-          true
+        case Const(c) => true
         case Op(e1, e2) =>
           // lemma instantiation
           val c1 = compile(e1)
           val c2 = compile(e2)
-          runAppendLemma((c1 ++ c2), Cons[ByteCode[A]](OpInst[A](), Nil[ByteCode[A]]()), S) &&
+          runAppendLemma((c1 ++ c2), Cons[ByteCode[A]](OpInst[A](), Nil()), S) &&
             runAppendLemma(c1, c2, S) &&
             compileInterpretEquivalenceLemma(e1, S) &&
             compileInterpretEquivalenceLemma(e2, Cons[A](interpret(e1), S))
       })
-  } holds
+  }.holds
 }