...

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 6b81ce60bf5b0d4e33280cd4cb3f7b596de045de..f1f64f8812d7ef427376482856e8fc88795f47da 100644 (file)
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -20,10 +20,11 @@ include "nat/minus.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: qpowerclass support;
-   class: support → qpowerclass A;
+   class: unary_morphism1 (setoid1_of_setoid support) (qpowerclass_setoid A);
    inhabited: ∀i. i ∈ indexes → class i ≬ class i;
    disjoint: ∀i,j. i ∈ indexes → j ∈ indexes → class i ≬ class j → i=j;
    covers: big_union support ? ? (λx.class x) = full_set A
@@ -55,7 +56,21 @@ nlemma partition_splits_card:
 ##| #y; #_;
     ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #Hc;
     ngeneralize in match (Hc y I) in ⊢ ?; *; #index; *; #Hi1; #Hi2;
-    nelim daemon
+    ngeneralize in match (f_sur ???? f ? Hi1) in ⊢ ?; *; #nindex; *; #Hni1; #Hni2;
+    ngeneralize in match (f_sur ???? (fi nindex) y ?) in ⊢ ?
+     [##2: napply (. #‡(†?));##[##3: napply Hni2 |##2: ##skip | nassumption]##]
+    *; #nindex2; *; #Hni21; #Hni22;
+    napply (ex_intro … (plus (big_plus nindex (λi.λ_.s i)) nindex2)); napply conj
+     [ nwhd in Hni1; nelim daemon
+     | nwhd in ⊢ (???%?);
+       (* BEL POSTO DOVE FARE UN LEMMA *)
+       (* invariante: Hni1; altre premesse: Hni1, Hni22 *)
+       nchange in Hni1 with (nindex < n); ngeneralize in match Hni1 in ⊢ ?;
+       nelim n
+        [ #A (* decompose *)
+        | #index'; #Hrec; 
+        ]
+     ]
   | #x; #x'; nnormalize in ⊢ (? → ? → %);
     nelim daemon
   ]