diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index 6854abb5a..21693824a 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -484,19 +484,35 @@ struct add_inductive_fn {
             return false;
         }
         // We have only one introduction rule, the final check is, the type of each argument
-        // that is not a parameter must live in Type.{0}.
+        // that is not a parameter:
+        //  1- It must live in Type.{0}, *OR*
+        //  2- It must occur in the return type. (this is essentially what is called a non-uniform parameter in Coq).
+        //     We can justify 2 by observing that this information is not a *secret* it is part of the type.
+        //     By eliminating to a non-proposition, we would not be revealing anything that is not already known.
         auto ir    = head(inductive_decl_intros(head(m_decls)));
         expr t     = intro_rule_type(ir);
         unsigned i = 0;
+        buffer<expr> to_check; // arguments that we must check if occur in the result type
         while (is_pi(t)) {
+            expr local = mk_local_for(t);
             if (i >= m_num_params) {
                 expr s = ensure_type(binding_domain(t));
-                if (!is_zero(sort_level(s)))
-                    return true;
+                if (!is_zero(sort_level(s))) {
+                    // Current argument is not in Type.{0} (i.e., condition 1 failed).
+                    // We save it in to_check to be able to try condition 2 above.
+                    to_check.push_back(local);
+                }
             }
-            t = instantiate(binding_body(t), mk_local_for(t));
+            t = instantiate(binding_body(t), local);
             i++;
         }
+        buffer<expr> result_args;
+        get_app_args(t, result_args);
+        // Check condition 2: every argument in to_check must occur in result_args
+        for (expr const & arg : to_check) {
+            if (std::find(result_args.begin(), result_args.end(), arg) == result_args.end())
+                return true; // condition 2 failed
+        }
         return false;
     }
 
diff --git a/tests/lean/acc.lean b/tests/lean/acc.lean
new file mode 100644
index 000000000..eb4fe2db0
--- /dev/null
+++ b/tests/lean/acc.lean
@@ -0,0 +1,6 @@
+import logic
+
+inductive acc (A : Type) (R : A → A → Prop) :  A → Prop :=
+intro : ∀ (x : A), (∀ (y : A), R y x → acc A R y) → acc A R x
+
+check @acc.rec
diff --git a/tests/lean/acc.lean.expected.out b/tests/lean/acc.lean.expected.out
new file mode 100644
index 000000000..6fabcafe2
--- /dev/null
+++ b/tests/lean/acc.lean.expected.out
@@ -0,0 +1,4 @@
+acc.rec :
+  Π {A : Type} {R : A → A → Prop} {C : A → Type},
+    (Π (x : A), (∀ (y : A), R y x → acc A R y) → (Π (y : A), R y x → C y) → C x) →
+    (Π {a : A}, acc A R a → C a)
diff --git a/tests/lua/ac.lua b/tests/lua/ac.lua
index e5b7852b2..adba24d30 100644
--- a/tests/lua/ac.lua
+++ b/tests/lua/ac.lua
@@ -14,4 +14,4 @@ function display_type(env, t)
    print(tostring(t) .. " : " .. tostring(type_checker(env):infer(t)))
 end
 
-display_type(env, Const({"Acc", "rec"}, {1}))
+display_type(env, Const({"Acc", "rec"}, {0, 1}))