diff --git a/tests/lean/run/term_app.lean b/tests/lean/run/term_app.lean
new file mode 100644
index 0000000000..c0088319f5
--- /dev/null
+++ b/tests/lean/run/term_app.lean
@@ -0,0 +1,14 @@
+inductive term
+| const : string → term
+| app   : string → list term → term
+
+/- TODO(Leo): remove after we fix bug in lemma generator. -/
+set_option eqn_compiler.lemmas false
+
+mutual def num_consts, num_consts_lst
+with num_consts : term → nat
+| (term.const n)  := 1
+| (term.app n ts) := num_consts_lst ts
+with num_consts_lst : list term → nat
+| []      := 0
+| (t::ts) := num_consts t + num_consts_lst ts