{M : Type u_1} →
  [inst : AddCommMonoid M] →
    {α : Type u_2} →
      DivisibleHull M →
        (f : M → ℕ+ → α) →
          (∀ (m m' : M) (s s' : ℕ+), DivisibleHull.mk m s = DivisibleHull.mk m' s' → f m s = f m' s') → α