diff --git a/tests/lean/conv.lean b/tests/lean/conv.lean
new file mode 100644
index 0000000000..f96da3a38c
--- /dev/null
+++ b/tests/lean/conv.lean
@@ -0,0 +1,22 @@
+
+
+
+Definition id (A : Type) : Type U := A.
+Variable p : (Int -> Int) -> Bool.
+Check fun (x : id Int), x.
+Variable f : (id Int) -> (id Int).
+Check p f.
+
+Definition c (A : Type 3) : Type 3 := Type 1.
+Variable g : (c (Type 2)) -> Bool.
+Variable a : (c (Type 1)).
+Check g a.
+
+Definition c2 {T : Type} (A : Type 3) (a : T) : Type 3 := Type 1
+Variable b : Int
+Check c2::explicit
+Variable g2 : (c2 (Type 2) b) -> Bool
+Check g2
+Variable a2 : (c2 (Type 1) b).
+Check g2 a2
+Check fun x : (c2 (Type 1) b), g2 x
\ No newline at end of file
diff --git a/tests/lean/conv.lean.expected.out b/tests/lean/conv.lean.expected.out
new file mode 100644
index 0000000000..5a971a7fd8
--- /dev/null
+++ b/tests/lean/conv.lean.expected.out
@@ -0,0 +1,19 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Defined: id
+  Assumed: p
+λ x : id ℤ, x : (id ℤ) → (id ℤ)
+  Assumed: f
+p f : Bool
+  Defined: c
+  Assumed: g
+  Assumed: a
+g a : Bool
+  Defined: c2
+  Assumed: b
+c2::explicit : Π (T : Type), Type 3 → T → Type 3
+  Assumed: g2
+g2 : (c2 Type 2 b) → Bool
+  Assumed: a2
+g2 a2 : Bool
+λ x : c2 Type 1 b, g2 x : (c2 Type 1 b) → Bool