diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp
index e0f8ee083d..cadaf99690 100644
--- a/src/library/compiler/lcnf.cpp
+++ b/src/library/compiler/lcnf.cpp
@@ -132,6 +132,11 @@ public:
                 minor = instantiate_rev(minor, minor_fvars.size(), minor_fvars.data());
                 if (j < num_fields) {
                     minor = eta_expand(minor, num_fields - j);
+                    for (; j < num_fields; j++) {
+                        expr new_fvar = m_lctx.mk_local_decl(ngen(), binding_name(minor), binding_domain(minor), binding_info(minor));
+                        minor_fvars.push_back(new_fvar);
+                        minor = instantiate(binding_body(minor), new_fvar);
+                    }
                 }
                 flet<cache> save_cache(m_cache, m_cache);
                 unsigned old_fvars_size    = m_fvars.size();
diff --git a/tests/lean/lcnf_bug1.lean b/tests/lean/lcnf_bug1.lean
new file mode 100644
index 0000000000..57a69874a8
--- /dev/null
+++ b/tests/lean/lcnf_bug1.lean
@@ -0,0 +1,5 @@
+set_option trace.compiler.lcnf true
+set_option pp.binder_types false
+
+def tst1 (a : nat) : nat :=
+@nat.cases_on (λ _, nat) a 0 id
diff --git a/tests/lean/lcnf_bug1.lean.expected.out b/tests/lean/lcnf_bug1.lean.expected.out
new file mode 100644
index 0000000000..868a065616
--- /dev/null
+++ b/tests/lean/lcnf_bug1.lean.expected.out
@@ -0,0 +1,2 @@
+[compiler.lcnf] tst1
+λ a, let _x_3 := nat.cases_on a (let _x_1 := nat.has_zero.0 in _x_1) (λ a, let _x_2 := id a in _x_2) in _x_3