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