fact: Definition whiskerTL {f : x $-> x00} (s : Square f01 f21 f10 f12) : Square (f01 $o f) f21 (f10 $o f) f12 := (cat_assoc _ _ _)^$ $@ (s $@R f) $@ cat_assoc _ _ _.
imports: Basics.Overture WildCat.Core WildCat.Equiv