diff --git a/tests/lean/run/inv_bug2.lean b/tests/lean/run/inv_bug2.lean
index 501c78be1..24a891e34 100644
--- a/tests/lean/run/inv_bug2.lean
+++ b/tests/lean/run/inv_bug2.lean
@@ -7,7 +7,7 @@ namespace vector
   protected definition destruct2 (v : vector A (succ (succ n))) {P : Π {n : nat}, vector A (succ n) → Type}
                                  (H : Π {n : nat} (h : A) (t : vector A n), P (h :: t)) : P v :=
   begin
-    cases v with (h', n', t'),
+    cases v with (n', h', t'),
     apply (H h' t')
   end
 end vector