{M : Type u_1} →
  {inst : Monoid M} →
    {N : Type u_2} →
      {inst_1 : Monoid N} →
        {φ : M →* N} →
          {A : Type u_4} →
            {inst_2 : AddMonoid A} →
              {inst_3 : DistribMulAction M A} →
                {B : Type u_5} →
                  {inst_4 : AddMonoid B} →
                    {inst_5 : DistribMulAction N B} →
                      {P : Sort u} →
                        {toMulActionHom : A →ₑ[⇑φ] B} →
                          {map_zero' : toMulActionHom.toFun 0 = 0} →
                            {map_add' :
                                ∀ (x y : A),
                                  toMulActionHom.toFun (x + y) = toMulActionHom.toFun x + toMulActionHom.toFun y} →
                              {toMulActionHom' : A →ₑ[⇑φ] B} →
                                {map_zero'' : toMulActionHom'.toFun 0 = 0} →
                                  {map_add'' :
                                      ∀ (x y : A),
                                        toMulActionHom'.toFun (x + y) =
                                          toMulActionHom'.toFun x + toMulActionHom'.toFun y} →
                                    { toMulActionHom := toMulActionHom, map_zero' := map_zero', map_add' := map_add' } =
                                        { toMulActionHom := toMulActionHom', map_zero' := map_zero'',
                                          map_add' := map_add'' } →
                                      (toMulActionHom ≍ toMulActionHom' → P) → P