ncoercion mcarr' : ∀A. ∀M: magma A. carr1 (qpowerclass_setoid (mtcarr A))
≝ λA.λM: magma A.mcarr ? M
on _M: magma ? to carr1 (qpowerclass_setoid (mtcarr ?)).
ncoercion mcarr' : ∀A. ∀M: magma A. carr1 (qpowerclass_setoid (mtcarr A))
≝ λA.λM: magma A.mcarr ? M
on _M: magma ? to carr1 (qpowerclass_setoid (mtcarr ?)).