X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fpartitions.ma;h=de29e796c47141fc80cd8659aa35a64c68e01a82;hb=8e15fc948d1c5dafb982701790fb085f34a7dd10;hp=dde57de058ce45406b15c78e580cee79daee1ce6;hpb=6d0664747588f771e953c4d70f96e1cb5953d60e;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index dde57de05..de29e796c 100644
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -78,7 +78,7 @@ ntheorem iso_nat_nat_union_char:
     ncases (ltb_cases m (s (S n'))); *; #H1; #H2; nrewrite > H2;
     nwhd in ⊢ (let p ≝ % in ?); nwhd
      [ napply conj [napply conj
-        [ nwhd in ⊢ (????(?(?%(λ_.λ_:(??%).?))%)); nrewrite > (minus_canc n'); napply refl
+        [ nwhd in ⊢ (???(?(?%(λ_.λ_:(??%).?))%)); nrewrite > (minus_canc n'); napply refl
         | nnormalize; napply le_n]
       ##| nnormalize; nassumption ]
    ##| nchange in H with (m < s (S n') + big_plus (S n') (λi.λ_.s i));
@@ -88,7 +88,7 @@ ntheorem iso_nat_nat_union_char:
         |@
          [nrewrite > (split_big_plus …); ##[##2:napply ad_hoc11;##|##3:##skip]
           nrewrite > (ad_hoc12 …); ##[##2: nassumption]
-          nwhd in ⊢ (????(?(??%)?));
+          nwhd in ⊢ (???(?(??%)?));
           nrewrite > (ad_hoc13 …);##[##2: nassumption]
           napply ad_hoc14 [ napply not_lt_to_le; nassumption ]
           nwhd in ⊢ (???(?(??%)?));