{α : Type u_1} →
  {C : Multiset α → Sort u_3} →
    (m : Multiset α) →
      C 0 →
        (C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)) →
          (∀ (a a' : α) (m : Multiset α) (b : C m),
              C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)) →
            C m