a b c d e f (g : e $-> _) : f $== fmap01 cat_tensor a (twist c b d) $o g -> fmap01 cat_tensor a (twist b c d) $o f $== g. Proof. intros p; symmetry; apply moveL_fmap01_twistL; symmetry; exact p. Defined.
Require Import Basics.Overture Basics.Tactics Types.Forall WildCat.Monoidal. Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv. Require Import WildCat.NatTrans WildCat.Square WildCat.Opposite.