1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
TrM.A = M.A : Set TrM.A is monomorphic OpM.A = M.A : Set OpM.A is monomorphic TrM.B = M.B : Set TrM.B is monomorphic *** [ OpM.B : Set ] OpM.B is monomorphic