{B : Type u_1} →
  {M : CoxeterMatrix B} →
    {W : Type u_2} →
      {inst : Group W} →
        {P : Sort u} →
          {mulEquiv mulEquiv' : W ≃* M.Group} →
            { mulEquiv := mulEquiv } = { mulEquiv := mulEquiv' } → (mulEquiv ≍ mulEquiv' → P) → P