include "nat/minus.ma".
include "datatypes/pairs.ma".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
+alias symbol "eq" (instance 7) = "setoid1 eq".
nrecord partition (A: setoid) : Type[1] ≝
{ support: setoid;
indexes: ext_powerclass support;