]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/nlibrary/sets/partitions.ma
more auto
[helm.git] / helm / software / matita / nlibrary / sets / partitions.ma
index 95145b11b4e150ca6d1b86d9069fa2cc274f9c22..1bb482f6e1c1310b133b0f1508aee6e3857bf2b0 100644 (file)
@@ -21,6 +21,7 @@ include "datatypes/pairs.ma".
 alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid1 eq".
 alias symbol "eq" = "setoid eq".
+alias symbol "eq" = "setoid1 eq".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: ext_powerclass support;