diff --git a/vstte10competition/AmortizedQueue.scala b/vstte10competition/AmortizedQueue.scala
index 7968b415ed1c83b9f8f2d3652a71f55771f5367e..9c049989dd5a734e213307d14a609bf95bfdc474 100644
--- a/vstte10competition/AmortizedQueue.scala
+++ b/vstte10competition/AmortizedQueue.scala
@@ -92,10 +92,9 @@ object AmortizedQueue {
   @induct
   def propTail(rear : List, front : List, list : List, elem : Int) : Boolean = {
     require(!isEmpty(Queue(front, rear)) && isAmortized(Queue(front, rear)))
-    val queue = Queue(front, rear)
-    if (asList(queue) == list) {
+    if (asList(Queue(front, rear)) == list) {
       list match {
-        case Cons(_, xs) => asList(tail(queue)) == xs
+        case Cons(_, xs) => asList(tail(Queue(front, rear))) == xs
       }
     } else
       true