∀ (R : Type u_1) [inst : Rack R] (G : Type u_2) [inst_1 : Group G] (f : ShelfHom R (Quandle.Conj G))
  (g : Rack.EnvelGroup R →* G), f = (Quandle.Conj.map g).comp (Rack.toEnvelGroup R) → g = Rack.toEnvelGroup.map f