(f01 : x00 $<~> x02) (f21 : x20 $<~> x22) (s : Square f01 f21 f10 f12) : Square (f01^-1$) (f21^-1$) f12 f10 := transpose (hinverse _ _ (transpose s)).
Require Import Basics.Overture. Require Import WildCat.Core. Require Import WildCat.Equiv.