diff --git a/tests/lean/run/crash.lean b/tests/lean/crash.lean
similarity index 100%
rename from tests/lean/run/crash.lean
rename to tests/lean/crash.lean
diff --git a/tests/lean/crash.lean.expected.out b/tests/lean/crash.lean.expected.out
new file mode 100644
index 000000000..023223ef5
--- /dev/null
+++ b/tests/lean/crash.lean.expected.out
@@ -0,0 +1,6 @@
+crash.lean:6:0: error: type mismatch at application
+  (λ (H' : not P), _) H
+expected type:
+  not P
+given type:
+  P