ok, but slow on includes

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 775cbd390c4ec9287fba0148c22ebe0014d0e776..3e4cb942b4c09ba22e4188c3239748a915968fba 100644 (file)
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -24,6 +24,7 @@ nrecord magma (A: magma_type) : Type[1] ≝
    op_closed: ∀x,y. x ∈ mcarr → y ∈ mcarr → op A x y ∈ mcarr
  }.
 
+alias symbol "hint_decl" = "hint_decl_Type2".
 unification hint 0 ≔ 
   A : ? ⊢ carr1 (qpowerclass_setoid A) ≡ qpowerclass A. 
 

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 3b17099a371474318101168301daff9fe23a31ef..e83175f18921ac5675134fda93b77ce979ed9d69 100644 (file)
--- 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) …);