{G H : ZeroGpd} (f : G $<~> H) (x : H) (y : G) (p : x $== equiv_fun_0gpd f y) : equiv_fun_0gpd f^-1$ x $== y := fmap (equiv_fun_0gpd f^-1$) p $@ cat_eissect f y.
Require Import Basics.Overture Basics.Tactics Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd