(s : Square f01 f21 f10 f12) (t : Square f21 f41 f30 f32) : Square f01 f41 (f30 $o f10) (f32 $o f12) := (cat_assoc _ _ _)^$ $@ (t $@R f10) $@ cat_assoc _ _ _ $@ (f32 $@L s) $@ (cat_assoc _ _ _)^$.
Require Import Basics.Overture. Require Import WildCat.Core. Require Import WildCat.Equiv.