diff --git a/tests/lean/run/def_ite_value.lean b/tests/lean/run/def_ite_value.lean
new file mode 100644
index 0000000000..2815a36a97
--- /dev/null
+++ b/tests/lean/run/def_ite_value.lean
@@ -0,0 +1,21 @@
+set_option new_elaborator true
+
+inductive bv : nat → Type
+| nil  : bv 0
+| cons : Π n, bool → bv n → bv (n+1)
+
+open bv
+
+definition f : ∀ n : nat, bv n → nat → nat
+| (n+1) (cons .n b v) 1000000 := f n v 0
+| (n+1) (cons .n b v) x      := f n v (x + 1)
+| _     _             _      := 1
+
+set_option pp.binder_types true
+
+check @f._main.equations.eqn_1
+check @f._main.equations.eqn_2
+check @f._main.equations.eqn_3
+
+example (n : nat) (b : bool) (v : bv n) (x : nat) : x ≠ 1000000 → f (n+1) (cons n b v) x = f n v (x + 1) :=
+assume H, f._main.equations.eqn_3 n b v x H