diff --git a/hott/arity.hlean b/hott/arity.hlean
index cac814dbe..954e0f6ee 100644
--- a/hott/arity.hlean
+++ b/hott/arity.hlean
@@ -134,8 +134,7 @@ namespace funext
              begin
                intro H, esimp [apD100, eq_of_homotopy2, function.compose],
                apply eq_of_homotopy, intro a,
-               apply concat, apply (ap (λx, @apD10 _ (λb : B a, _) _ _ (x a))), apply (retr apD10),
---TODO: remove implicit argument after #469 is closed
+               apply concat, apply (ap (λx, apD10 (x a))), apply (retr apD10),
                apply (retr apD10)
              end
              begin