diff --git a/tests/lean/run/doNotation2.lean b/tests/lean/run/doNotation2.lean
index 0fed9216c7..9b168186e9 100644
--- a/tests/lean/run/doNotation2.lean
+++ b/tests/lean/run/doNotation2.lean
@@ -30,3 +30,17 @@ rfl
 
 theorem ex2 : (g [] $.run' 0) = 1 :=
 rfl
+
+def h (x : Nat) (y : Nat) : Nat := do
+if x > 0 then
+  let y := x + 1 -- this is a new `y` that shadows the one above
+  x := y
+else
+  y := y + 1
+return x + y
+
+theorem ex3 (y : Nat) : h 0 y = 0 + (y + 1) :=
+rfl
+
+theorem ex4 (y : Nat) : h 1 y = (1 + 1) + y :=
+rfl