fact: Definition compose_cate_assoc {A} `{HasEquivs A} {a b c d : A} (f : a $<~> b) (g : b $<~> c) (h : c $<~> d) : cate_fun ((h $oE g) $oE f) $== cate_fun (h $oE (g $oE f)).
imports: Basics.Utf8 Basics.Overture Basics.Tactics WildCat.Core