+
+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 ?)).
+*)
+