a b c d f (g : _ $-> d) : f $== g $o twist b a c -> f $o twist a b c $== g. Proof. intros p; symmetry; apply moveL_twistR; 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.