diff --git a/tests/lean/916.lean b/tests/lean/916.lean
new file mode 100644
index 0000000000..7223b859ab
--- /dev/null
+++ b/tests/lean/916.lean
@@ -0,0 +1,4 @@
+example : Id Nat := do
+  let mut x := 1
+  have x : Nat := 2
+  x
diff --git a/tests/lean/916.lean.expected.out b/tests/lean/916.lean.expected.out
new file mode 100644
index 0000000000..1de8b68bfb
--- /dev/null
+++ b/tests/lean/916.lean.expected.out
@@ -0,0 +1 @@
+916.lean:3:2-3:19: error: mutable variable 'x' cannot be shadowed