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