...

[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 93f9cd6b5d3e014121adf9ff04042816848cb5a6..1dce8d535f0926646958a8224412065e55dc1ea3 100644 (file)
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -25,6 +25,8 @@ alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid1 eq".
 alias symbol "eq" = "setoid eq".
+alias symbol "eq" = "setoid1 eq".
+alias symbol "eq" = "setoid eq".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: qpowerclass support;
@@ -165,28 +167,29 @@ napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
        nlapply
         (iso_nat_nat_union_uniq n s nindex (fst … (iso_nat_nat_union s xxx n))
           nindex2 (snd … (iso_nat_nat_union s xxx n)) ?????)
-        [##2: *; #E1; #E2; nrewrite > E1; nrewrite > E2; napply refl
-        | napply le_S_S_to_le; nassumption
+        [##6: *; #E1; #E2; nrewrite > E1; nrewrite > E2; napply refl
+        |##5: napply le_S_S_to_le; nassumption
         |##*: nassumption]##]
 ##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E;
-    ngeneralize in match (? : ∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ pc ? (Nat_ (s i1)) → i2' ∈ pc ? (Nat_ (s i1')) → eq_rel (carr A) (eq A) (iso_f ???? (fi i1) i2) (iso_f ???? (fi i1') i2') → i1=i1' ∧ i2=i2') in ⊢ ?
-     [##2: #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E;
-      ngeneralize in match (disjoint ? P (iso_f ???? f i1) (iso_f ???? f i1') ???) in ⊢ ?
+    ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ pc ? (Nat_ (s i1)) → i2' ∈ pc ? (Nat_ (s i1')) → eq_rel (carr A) (eq A) (iso_f ???? (fi i1) i2) (iso_f ???? (fi i1') i2') → i1=i1' ∧ i2=i2');
+    ##[ #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E;
+       nlapply(disjoint … P (f i1) (f i1') ???)
        [##2,3: napply f_closed; nassumption
-       |##4: napply ex_intro [ napply (iso_f ???? (fi i1) i2) ] napply conj
-         [ napply f_closed; nassumption ##| napply (. ?‡#) [ nassumption | ##2: ##skip]
-         nwhd; napply f_closed; nassumption]##]
-      #E'; ngeneralize in match (? : i1=i1') in ⊢ ?
-       [##2: napply (f_inj … E'); nassumption
-       | #E''; nrewrite < E''; napply conj
-          [ napply refl | nrewrite < E'' in E; #E'''; napply (f_inj … E''')
+       |##1: @ (fi i1 i2); @;
+         ##[ napply f_closed; nassumption ##| alias symbol "refl" = "refl1".
+napply (. E‡#);
+             nwhd; napply f_closed; nassumption]##]
+      #E'; ncut(i1 = i1'); ##[ napply (f_inj … E'); nassumption; ##]
+      #E''; nrewrite < E''; @; 
+      ##[ @;
+      ##| nrewrite < E'' in E; #E'''; napply (f_inj … E''')
              [ nassumption | nrewrite > E''; nassumption ]##]##]
    ##] #K;
     nelim (iso_nat_nat_union_char n s x Hx); *; #i1x; #i2x; #i3x;
     nelim (iso_nat_nat_union_char n s x' Hx'); *; #i1x'; #i2x'; #i3x';
-    ngeneralize in match (K … E) in ⊢ ?
-     [##2,3: napply le_to_le_S_S; nassumption
-     |##4,5: nassumption]
+    nlapply (K … E)  
+     [##1,2: nassumption;
+     ##|##3,4:napply le_to_le_S_S; nassumption; ##]
     *; #K1; #K2;
     napply (eq_rect_CProp0_r ?? (λX.λ_.? = X) ?? i1x');
     napply (eq_rect_CProp0_r ?? (λX.λ_.X = ?) ?? i1x);