diff --git a/src/kernel/quotient/quotient.cpp b/src/kernel/quotient/quotient.cpp
index d6dbe7fc6..27e3ce39a 100644
--- a/src/kernel/quotient/quotient.cpp
+++ b/src/kernel/quotient/quotient.cpp
@@ -82,6 +82,9 @@ optional<pair<expr, constraint_seq>> quotient_normalizer_extension::operator()(e
 
     expr const & f = args[mk_pos-2];
     expr r = mk_app(f, app_arg(mk));
+    unsigned elim_arity = mk_pos+1;
+    if (args.size() > elim_arity)
+        r = mk_app(r, args.size() - elim_arity, args.begin() + elim_arity);
     return some_ecs(r, mk_cs.second);
 }
 
diff --git a/tests/lean/quot_bug.lean b/tests/lean/quot_bug.lean
new file mode 100644
index 000000000..5ee072047
--- /dev/null
+++ b/tests/lean/quot_bug.lean
@@ -0,0 +1,9 @@
+open quot
+variables {A : Type} {B : A → Type}
+
+variable f : Π a : A, B a
+
+eval λ x, quot.lift_on ⟦f⟧ (λf : (Πx : A, B x), f) _ x
+
+example (x : A) : quot.lift_on ⟦f⟧ (λf : (Πx : A, B x), f) sorry x = f x :=
+rfl
diff --git a/tests/lean/quot_bug.lean.expected.out b/tests/lean/quot_bug.lean.expected.out
new file mode 100644
index 000000000..13e60ba80
--- /dev/null
+++ b/tests/lean/quot_bug.lean.expected.out
@@ -0,0 +1,2 @@
+λ (x : A), f x
+quot_bug.lean:8:59: warning: using 'sorry'