-(*ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid
- on _s: setoid to setoid1.*)
-(*prefer coercion Type_OF_setoid.*)
+alias symbol "hint_decl" = "hint_decl_CProp2".
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type2".
+unification hint 0 ≔ A,x,y;
+ T ≟ carr A,
+ R ≟ setoid1_of_setoid A,
+ T1 ≟ carr1 R
+(*-----------------------------------------------*) ⊢
+ eq_rel T (eq0 A) x y ≡ eq_rel1 T1 (eq1 R) x y.
+
+unification hint 0 ≔ A;
+ R ≟ setoid1_of_setoid A
+(*-----------------------------------------------*) ⊢
+ carr A ≡ carr1 R.