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