diff --git a/Theory/Natural/Transformation.v b/Theory/Natural/Transformation.v
index a0edb7ff..c23d9d78 100644
--- a/Theory/Natural/Transformation.v
+++ b/Theory/Natural/Transformation.v
@@ -46,10 +46,8 @@ Qed.
 End Transform.
 
 Arguments transform {_ _ _ _} _ _.
-Arguments naturality
-  {_ _ _ _ _ _ _ _}, {_ _ _ _} _ {_ _ _}, {_ _ _ _} _ _ _ _.
-Arguments naturality_sym
-  {_ _ _ _ _ _ _ _}, {_ _ _ _} _ {_ _ _}, {_ _ _ _} _ _ _ _.
+Arguments naturality {_ _ _ _} _ _ _ _.
+Arguments naturality_sym {_ _ _ _} _ _ _ _.
 
 Declare Scope transform_scope.
 Declare Scope transform_type_scope.
@@ -214,8 +212,8 @@ Program Definition whisker_right {C D : Category} {F G : C ⟶ D} `(N : F ⟹ G)
         {E : Category} (X : E ⟶ C) : F ◯ X ⟹ G ◯ X := {|
   transform := λ x, N (X x);
 
-  naturality     := λ _ _ _, naturality;
-  naturality_sym := λ _ _ _, naturality_sym
+  naturality     := λ _ _ _, naturality _ _ _ _;
+  naturality_sym := λ _ _ _, naturality_sym _ _ _ _
 |}.
 
 Notation "N ⊲ F" := (whisker_right N F) (at level 10).