diff --git a/tests/lean/eq2.lean b/tests/lean/eq2.lean
new file mode 100644
index 000000000..9c5ffeef4
--- /dev/null
+++ b/tests/lean/eq2.lean
@@ -0,0 +1,7 @@
+Variable List : Type -> Type
+Variable nil  {A : Type} : List A
+Variable cons {A : Type} (head : A) (tail : List A) : List A
+Variable l : List Int.
+Check l = nil.
+Set pp::implicit true
+Check l = nil.
diff --git a/tests/lean/eq2.lean.expected.out b/tests/lean/eq2.lean.expected.out
new file mode 100644
index 000000000..2a3c621c2
--- /dev/null
+++ b/tests/lean/eq2.lean.expected.out
@@ -0,0 +1,9 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: List
+  Assumed: nil
+  Assumed: cons
+  Assumed: l
+l = nil : Bool
+  Set: lean::pp::implicit
+eq::explicit (List ℤ) l (nil::explicit ℤ) : Bool