diff --git a/tests/lean/run/destruct.lean b/tests/lean/run/destruct.lean
index 23eef38b99..5f8a4c8146 100644
--- a/tests/lean/run/destruct.lean
+++ b/tests/lean/run/destruct.lean
@@ -26,5 +26,5 @@ begin
   intro n,
   destruct n,
    dsimp, intros, note h := lt_irrefl 0, cc,
-   dsimp, intros, subst n, reflexivity
+   dsimp, intros, subst n
 end