| napply trans]##]
nqed.
-ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid
- on _s: setoid to setoid1.
+(*ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid
+ on _s: setoid to setoid1.*)
(*prefer coercion Type_OF_setoid.*)
interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).