diff --git a/tests/lean/bad10.lean b/tests/lean/bad10.lean
new file mode 100644
index 000000000..ef57c1376
--- /dev/null
+++ b/tests/lean/bad10.lean
@@ -0,0 +1,8 @@
+SetOption pp::implicit true.
+SetOption pp::colors   false.
+Variable N : Type.
+
+Definition T (a : N) (f : _ -> _) (H : f a == a) : f (f _) == f _ :=
+SubstP (fun x : N, f (f a) == _) (Refl (f (f _))) H.
+
+Show Environment 1.
diff --git a/tests/lean/bad10.lean.expected.out b/tests/lean/bad10.lean.expected.out
new file mode 100644
index 000000000..0a75399dd
--- /dev/null
+++ b/tests/lean/bad10.lean.expected.out
@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Set: lean::pp::implicit
+  Set: pp::colors
+  Assumed: N
+  Defined: T
+Definition T (a : N) (f : N → N) (H : f a == a) : f (f a) == f (f a) :=
+    @SubstP N (f a) a (λ x : N, f (f a) == f (f a)) (@Refl N (f (f a))) H