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