Be more explicit in Functor/Traversable/Product.v

jwiegley · Jan 31, 2024 · 3fe04f4 · 3fe04f4
1 parent 284c4bd
commit 3fe04f4
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/Functor/Traversable/Product.v b/Functor/Traversable/Product.v
@@ -40,8 +40,8 @@ Proof.
     rewrite comp_assoc.
     rewrites.
     rewrite <- !comp_assoc.
-    pose proof (naturality[@sequence _ _ _ O _ X]) as X3; simpl in *.
-    pose proof (naturality[@sequence _ _ _ P _ X]) as X4; simpl in *.
+    pose proof (naturality[@sequence _ _ _ O _ X] _ _ f) as X3; simpl in *.
+    pose proof (naturality[@sequence _ _ _ P _ X] _ _ f) as X4; simpl in *.
     rewrite !comp_assoc.
     comp_left.
     rewrite bimap_fmap.
@@ -55,8 +55,8 @@ Proof.
     rewrite comp_assoc.
     rewrites.
     rewrite <- !comp_assoc.
-    pose proof (naturality[@sequence _ _ _ O _ X]) as X3; simpl in *.
-    pose proof (naturality[@sequence _ _ _ P _ X]) as X4; simpl in *.
+    pose proof (naturality[@sequence _ _ _ O _ X] _ _ f) as X3; simpl in *.
+    pose proof (naturality[@sequence _ _ _ P _ X] _ _ f) as X4; simpl in *.
     rewrite !comp_assoc.
     comp_left.
     rewrite bimap_fmap.