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