diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index 2a0db71c6..fb9509844 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -654,9 +654,9 @@ struct inductive_cmd_fn {
                 save_def_info(name(n, "cases_on"), pos);
                 if (has_eq && has_heq) {
                     if (optional<environment> new_env = mk_no_confusion(env, inductive_decl_name(d))) {
-                        env = *new_env;
-                        save_def_info(name{n, "no_confusion_type"}, pos);
-                        // save_def_info(name(n, "no_confusion"), pos);
+                       env = *new_env;
+                       save_def_info(name{n, "no_confusion_type"}, pos);
+                       save_def_info(name(n, "no_confusion"), pos);
                     }
                 }
                 // if (has_prod) {
diff --git a/src/library/definitional/cases_on.cpp b/src/library/definitional/cases_on.cpp
index 8c2e62c10..57bef3eee 100644
--- a/src/library/definitional/cases_on.cpp
+++ b/src/library/definitional/cases_on.cpp
@@ -125,7 +125,7 @@ environment mk_cases_on(environment const & env, name const & n) {
     for (unsigned i = 0; i < num_idx_major; i++)
         cases_on_params.push_back(rec_params[num_params + num_types + num_minors + i]);
 
-    // Ad minor premises to rec_params and rec_args
+    // Add minor premises to rec_params and rec_args
     i = num_params + num_types;
     for (auto const & d : idecls) {
         bool is_main = inductive::inductive_decl_name(d) == n;
@@ -139,8 +139,11 @@ environment mk_cases_on(environment const & env, name const & n) {
                 while (is_pi(minor_type)) {
                     expr local = mk_local(ngen.next(), binding_name(minor_type), binding_domain(minor_type),
                                           binding_info(minor_type));
-                    if (is_type_former_arg(C_names, binding_domain(minor_type))) {
-                        if (mlocal_name(get_app_fn(binding_domain(minor_type))) == C_main) {
+                    expr curr_type = mlocal_type(local);
+                    while (is_pi(curr_type))
+                        curr_type = binding_body(curr_type);
+                    if (is_type_former_arg(C_names, curr_type)) {
+                        if (mlocal_name(get_app_fn(curr_type)) == C_main) {
                             minor_params.push_back(local);
                         } else {
                             minor_params.push_back(update_mlocal(local, *unit));
diff --git a/tests/lean/run/ho.lean b/tests/lean/run/ho.lean
new file mode 100644
index 000000000..8daa9d9e3
--- /dev/null
+++ b/tests/lean/run/ho.lean
@@ -0,0 +1,11 @@
+import data.nat
+
+inductive star : Type₁ :=
+z  : star,
+s  : (nat → star) → star
+
+check @star.rec
+check @star.cases_on
+
+example (f : nat → star) : ¬ star.z = star.s f :=
+assume H, star.no_confusion H