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