fixed notation for \cup and \cap

[helm.git] / helm / software / matita / nlibrary / sets / partitions.ma

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 84d320e7f1f9763edf9ff4d3d55361cdab0fbebf..b92fe9ab3011d9bcbcb75637b51c886c43de6d05 100644 (file)
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -128,9 +128,9 @@ nlemma partition_splits_card:
     nlapply (Hc y I); *; #index; *; #Hi1; #Hi2;
     nlapply (f_sur ???? f ? Hi1); *; #nindex; *; #Hni1; #Hni2;
     nlapply (f_sur ???? (fi nindex) y ?)
-     [ alias symbol "refl" = "refl".
-alias symbol "prop1" = "prop11".
-alias symbol "prop2" = "prop21 mem".
+     [ alias symbol "refl" (instance 3) = "refl".
+alias symbol "prop2" (instance 2) = "prop21".
+alias symbol "prop1" (instance 4) = "prop11".
 napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
     *; #nindex2; *; #Hni21; #Hni22;
     nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2);