diff --git a/theories/Homotopy/ClassifyingSpace.v b/theories/Homotopy/ClassifyingSpace.v
index 94cd4fce13a..d4cf92a1b33 100644
--- a/theories/Homotopy/ClassifyingSpace.v
+++ b/theories/Homotopy/ClassifyingSpace.v
@@ -581,8 +581,7 @@ Proof.
     rapply pequiv_pclassifyingspace_pi1. }
   snrapply Build_NatEquiv.
   1: intro; exact pequiv_ptr_rec.
-  rapply (@is1natural_prewhisker _ _ _
-            (opyon (pTr 1 X)) (opyon X) B _ _ _ _ _ _ _ _ _ _ (opyoneda _ _ _)).
+  rapply (is1natural_prewhisker (G:=opyon X) B (opyoneda _ _ _)).
 Defined.
 
 (** The classifying space functor and the fundamental group functor form an adjunction (pType needs to be restricted to the subcategory of 0-connected pTypes). Note that the full adjunction should also be natural in X, but this was not needed yet. *)