diff --git a/tests/lean/run/reflectiveIndPred.lean b/tests/lean/run/reflectiveIndPred.lean
new file mode 100644
index 0000000000..09d484100a
--- /dev/null
+++ b/tests/lean/run/reflectiveIndPred.lean
@@ -0,0 +1,12 @@
+inductive Expr where
+  | val : Nat → Expr
+  | add : Expr → Expr → Expr
+  | fn  : (Nat → Expr) → Expr
+
+inductive Pos : Expr → Prop
+  | base : (n : Nat) → Pos (Expr.val n.succ)
+  | add  : Pos e₁ → Pos e₂ → Pos (Expr.add e₁ e₂)
+  | fn   : ((n : Nat) → Pos (f n)) → Pos (Expr.fn f)
+
+#print PosProofBelow
+#print Pos.brecOn