{f : x20 $<~> x} (s : Square f01 f21 f10 f12) : Square f01 (f21 $o f^-1$) (f $o f10) f12 := cat_assoc _ _ _ $@ (f21 $@L compose_V_hh _ _) $@ s.
Require Import Basics.Overture. Require Import WildCat.Core. Require Import WildCat.Equiv.