{M : Type u_1} →
  {inst : Mul M} →
    {P : Sort u} →
      {toSetoid : Setoid M} →
        {mul' : ∀ {w x y z : M}, toSetoid w x → toSetoid y z → toSetoid (w * y) (x * z)} →
          {toSetoid' : Setoid M} →
            {mul'' : ∀ {w x y z : M}, toSetoid' w x → toSetoid' y z → toSetoid' (w * y) (x * z)} →
              { toSetoid := toSetoid, mul' := mul' } = { toSetoid := toSetoid', mul' := mul'' } →
                (toSetoid ≍ toSetoid' → P) → P