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