diff --git a/src/kernel/quotient/quotient.cpp b/src/kernel/quotient/quotient.cpp
index 27e3ce39a..5983a9e7e 100644
--- a/src/kernel/quotient/quotient.cpp
+++ b/src/kernel/quotient/quotient.cpp
@@ -59,10 +59,13 @@ optional<pair<expr, constraint_seq>> quotient_normalizer_extension::operator()(e
     if (!ext.m_initialized)
         return none_ecs();
     unsigned mk_pos;
+    unsigned arg_pos;
     if (const_name(fn) == *g_quotient_lift) {
-        mk_pos = 5;
+        mk_pos  = 5;
+        arg_pos = 3;
     } else if (const_name(fn) == *g_quotient_ind) {
-        mk_pos = 4;
+        mk_pos  = 4;
+        arg_pos = 3;
     } else {
         return none_ecs();
     }
@@ -80,7 +83,7 @@ optional<pair<expr, constraint_seq>> quotient_normalizer_extension::operator()(e
     if (const_name(mk_fn) != *g_quotient_mk)
         return none_ecs();
 
-    expr const & f = args[mk_pos-2];
+    expr const & f = args[arg_pos];
     expr r = mk_app(f, app_arg(mk));
     unsigned elim_arity = mk_pos+1;
     if (args.size() > elim_arity)
diff --git a/tests/lean/quot_ind_bug.lean b/tests/lean/quot_ind_bug.lean
new file mode 100644
index 000000000..31b060c78
--- /dev/null
+++ b/tests/lean/quot_ind_bug.lean
@@ -0,0 +1,6 @@
+open quot
+
+variables {A : Type} [s : setoid A] {B : quot s → Prop} (c : ∀ (a : A), B (quot.mk a)) (a : A)
+check quot.ind c ⟦a⟧
+check c a
+eval quot.ind c ⟦a⟧
diff --git a/tests/lean/quot_ind_bug.lean.expected.out b/tests/lean/quot_ind_bug.lean.expected.out
new file mode 100644
index 000000000..f8d085512
--- /dev/null
+++ b/tests/lean/quot_ind_bug.lean.expected.out
@@ -0,0 +1,3 @@
+ind c ⟦a⟧ : B ⟦a⟧
+c a : B ⟦a⟧
+c a