∀ {M : Type u_4} {N : Type u_2} {φ : M → N} {X : Type u_1} [inst : VAdd M X] {Y : Type u_3} [inst_1 : VAdd N Y]
  (f : X →ₑ[φ] Y) (g : Y → X), Function.RightInverse g ⇑f → ∀ (m : N) (x : Y), g (m +ᵥ x) = g (m +ᵥ f (g x))