{A} `{HasEquivs A} {a b c : A} (e : b $<~> c) (f : a $-> c) (g : a $-> b) (p : e^-1$ $o f $== g) : f $== e $o g := cate_moveL_eM (A:=A^op) (a:=c) (b:=b) (c:=a) e f g p.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.