diff --git a/src/kernel/inductive.h b/src/kernel/inductive.h
index e3de55a073..ca19a674ea 100644
--- a/src/kernel/inductive.h
+++ b/src/kernel/inductive.h
@@ -55,13 +55,17 @@ inline optional<expr> inductive_reduce_rec(environment const & env, expr const &
     if (!rule) return none_expr();
     buffer<expr> major_args;
     get_app_args(major, major_args);
-    if (rec_val.get_nparams() + rule->get_nfields() != major_args.size()) return none_expr();
+    if (rule->get_nfields() > major_args.size()) return none_expr();
     if (length(const_levels(rec_fn)) != length(rec_info.get_lparams())) return none_expr();
     expr rhs = instantiate_lparams(rule->get_rhs(), rec_info.get_lparams(), const_levels(rec_fn));
     /* apply parameters, motives and minor premises from recursor application. */
     rhs      = mk_app(rhs, rec_val.get_nparams() + rec_val.get_nmotives() + rec_val.get_nminors(), rec_args.data());
+    /* The number of parameters in the constructor is not necessarily
+       equal to the number of parameters in the recursor when we have
+       nested inductive types. */
+    unsigned nparams = major_args.size() - rule->get_nfields();
     /* apply fields from major premise */
-    rhs      = mk_app(rhs, rule->get_nfields(), major_args.data() + rec_val.get_nparams());
+    rhs      = mk_app(rhs, rule->get_nfields(), major_args.data() + nparams);
     if (rec_args.size() > major_idx + 1) {
         /* recursor application has more arguments after major premise */
         unsigned nextra = rec_args.size() - major_idx - 1;