diff --git a/tests/lean/run/let1.lean b/tests/lean/run/let1.lean
new file mode 100644
index 0000000000..38cb8b8dff
--- /dev/null
+++ b/tests/lean/run/let1.lean
@@ -0,0 +1,10 @@
+import standard
+
+check
+  let f x y := x ∧ y,
+      g x   := f x x,
+      a     := g true
+  in  λ (x : a),
+        let h x y := f x (g y),
+            b     := h
+        in b