X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fpartitions.ma;h=e83175f18921ac5675134fda93b77ce979ed9d69;hb=32f2a8f8016b2c6c7fb88189fc0ea0c7f9336555;hp=3b17099a371474318101168301daff9fe23a31ef;hpb=f5f35ef830b1335dad2fcc3c1aae2b57815f73b1;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 3b17099a3..e83175f18 100644
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "sets/sets.ma".
-include "nat/plus.ma".
+include "nat/plus.ma". (* tempi biblici neggli include che fa plus.ma *)
 include "nat/compare.ma".
 include "nat/minus.ma".
 include "datatypes/pairs.ma".
@@ -26,6 +26,7 @@ alias symbol "eq" = "setoid1 eq".
 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;
@@ -114,10 +115,7 @@ ntheorem iso_nat_nat_union_pre:
   [##2: napply le_to_le_S_S; nassumption]
  napply ad_hoc15
   [ nwhd in ⊢ (???(?%?));
-  
-    napply (eq_rect_CProp0_r nat (n - i1) (λx.λy.?) ?? (minus_S_S …)); STOP
-  
-    nrewrite > (minus_S_S n i1); napply big_plus_preserves_ext; #i; #_;
+    napply big_plus_preserves_ext; #i; #_;
     nrewrite > (plus_n_S i i1); napply refl
   | nrewrite > (split_big_plus (S i1) i1 (λi.λ_.s i) ?) [##2: napply le_S; napply le_n]
     napply ad_hoc16; nrewrite > (minus_S i1); nnormalize; nrewrite > (plus_n_O (s i1) …);