diff --git a/tests/lean/hott/inj_tac.hlean b/tests/lean/hott/inj_tac.hlean
index 622bb11238..1b8be6c595 100644
--- a/tests/lean/hott/inj_tac.hlean
+++ b/tests/lean/hott/inj_tac.hlean
@@ -11,7 +11,7 @@ end
 example (A : Type) (n : nat) (v w : vector A n) (a : A) (b : A) :
         a :: v = b :: w →  b = a :=
 begin
-  intro H, injection H with aeqb beqw,
+  intro H, injection H with aeqb neqn beqw,
   rewrite aeqb
 end