{A B : Type} {tensorA : A -> A -> A} {tensorB : B -> B -> B} {IA : A} {IB : B} (F : A -> B) `{IsMonoidalFunctor A B tensorA tensorB IA IB F} {x x' y : A} (f : x $-> x') : fmap_tensor F (x', y) $o fmap10 tensorB (fmap F f) (F y) $== fmap F (fmap10 tensorA f y) $o fmap_tensor F (x, y). Proof. refine ((_ $@L (fmap12 tensorB _ (fmap_id _ _) $@ fmap10_is_fmap11 _ _ _)^$) $@ _). refine (_ $@ (fmap2 F (fmap10_is_fmap11 _ _ _) $@R _)). snrapply fmap_tensor_nat. Defined.
Require Import Basics.Overture Basics.Tactics Types.Forall. Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv. Require Import WildCat.NatTrans WildCat.Opposite.