{M : Type u_8} →
  {N : Type u_9} →
    {φ : M → N} →
      {X : Type u_10} →
        {inst : VAdd M X} →
          {Y : Type u_11} →
            {inst_1 : VAdd N Y} →
              {P : Sort u} →
                {toFun : X → Y} →
                  {map_vadd' : ∀ (m : M) (x : X), toFun (m +ᵥ x) = φ m +ᵥ toFun x} →
                    {toFun' : X → Y} →
                      {map_vadd'' : ∀ (m : M) (x : X), toFun' (m +ᵥ x) = φ m +ᵥ toFun' x} →
                        { toFun := toFun, map_vadd' := map_vadd' } = { toFun := toFun', map_vadd' := map_vadd'' } →
                          (toFun ≍ toFun' → P) → P