\lambda M1,M2:CSemiGroup. \lambda x:ProdCSetoid (csg_crr M1) (csg_crr M2).
\lambda y:ProdCSetoid (csg_crr M1) (csg_crr M2).
match x with
\lambda M1,M2:CSemiGroup. \lambda x:ProdCSetoid (csg_crr M1) (csg_crr M2).
\lambda y:ProdCSetoid (csg_crr M1) (csg_crr M2).
match x with