∀ (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] (s t : Set α),
  VAddAssocClass (↥(fixingAddSubgroup (↥(fixingAddSubgroup M s)) (Subtype.val ⁻¹' t))) (↥(fixingAddSubgroup M s)) α