fact: Definition compose_h_Vh {A} `{HasEquivs A} {a b c : A} (f : c $<~> b) (g : a $-> b) : f $o (f^-1$ $o g) $== g := (cat_assoc _ _ _)^$ $@ (cate_isretr f $@R g) $@ cat_idl g.
imports: Basics.Utf8 Basics.Overture Basics.Tactics WildCat.Core