diff --git a/tests/lean/run/ginductive_pred.lean b/tests/lean/run/ginductive_pred.lean
new file mode 100644
index 0000000000..2db4af17d8
--- /dev/null
+++ b/tests/lean/run/ginductive_pred.lean
@@ -0,0 +1,14 @@
+inductive term : Type
+| var : nat → term
+| app : string → list term → term
+
+/- In the current system, it will be hard to work with mutually inductive predicates.
+   Reason: we cannot use well-founded recursion, and the induction principle for it
+   is too weak. -/
+mutual inductive var_occ, var_occ_list
+with var_occ : nat → term → Prop
+| leaf (n : nat) : var_occ n (term.var n)
+| app  (n : nat) (s : string) (ts : list term) : var_occ_list n ts → var_occ n (term.app s ts)
+with var_occ_list : nat → list term → Prop
+| head (n : nat) (t : term) (ts : list term) : var_occ n t → var_occ_list n (t::ts)
+| tail (n : nat) (t : term) (ts : list term) : var_occ_list n ts → var_occ_list n (t::ts)