-nrecord pre_magma_morphism (A,B: pre_magma) : Type ≝
- { mmcarr:1> A → B;
- mmprop: ∀x,y. mmcarr (op ? x y) = op ? (mmcarr x) (mmcarr y)
- }.
+alias symbol "hint_decl" = "hint_decl_Type2".
+unification hint 0 ≔
+ A : ? ⊢ carr1 (ext_powerclass_setoid A) ≡ ext_powerclass A.
+
+(*
+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 ?)).
+*)