∀ {G : Type u_1} {G' : Type u_2} {α : Type u_3} {β : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup G']
  [inst_2 : AddAction G β] [inst_3 : AddAction G' β] [VAddCommClass G G' β], VAddCommClass G G' (α ↪ β)