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