From cb5b07093fd98a1f715751695fc1388a3e3cbfb7 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 23 Apr 2015 15:38:15 -0400
Subject: [PATCH] fix(arity): remove unnecessary implicit arguments

---
 hott/arity.hlean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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