fact: Definition isinj_equiv_0gpd {G H : ZeroGpd} (f : G $<~> H) {x y : G} (h : equiv_fun_0gpd f x $== equiv_fun_0gpd f y) : x $== y.
imports: Basics.Overture Basics.Tactics WildCat.Core WildCat.Equiv WildCat.EquivGpd WildCat.Prod