TrM.A = N.A
     : Set
OpM.A = N.A
     : Set
TrM.B = N.B
     : Set
*** [ OpM.B : Set ]