remove an unnecessary premise from big_opM_own_1
The way big_opM_own_1
was stated, it requires an element of type B
, which is totally unnecessary.
The way big_opM_own_1
was stated, it requires an element of type B
, which is totally unnecessary.