{A} `{HasEquivs A} {a b c : A} (f : c $<~> b) (g : a $-> b) : f $o (f^-1$ $o g) $== g := (cat_assoc_opp _ _ _) $@ (cate_isretr f $@R g) $@ cat_idl g.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.