diff --git a/tests/lean/ty2.lean b/tests/lean/ty2.lean
new file mode 100644
index 000000000..f07cbfc64
--- /dev/null
+++ b/tests/lean/ty2.lean
@@ -0,0 +1,6 @@
+Definition B : Type   := Bool
+Definition T : Type 1 := Type
+Variable N : T
+Variable x : N
+Variable a : B
+Axiom H : a
diff --git a/tests/lean/ty2.lean.expected.out b/tests/lean/ty2.lean.expected.out
new file mode 100644
index 000000000..53dc668cd
--- /dev/null
+++ b/tests/lean/ty2.lean.expected.out
@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Defined: B
+  Defined: T
+  Assumed: N
+  Assumed: x
+  Assumed: a
+  Assumed: H