fact: Definition move_left_bottom {f12 : x02 $-> x} {f12' : x $-> x22} (s : Square f01 f21 f10 (f12' $o f12)) : Square (f12 $o f01) f21 f10 f12' := s $@ cat_assoc _ _ _.
imports: Basics.Overture WildCat.Core WildCat.Equiv