Different aliases, better equality inferred.

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index dde57de058ce45406b15c78e580cee79daee1ce6..de29e796c47141fc80cd8659aa35a64c68e01a82 100644 (file)
--- 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 ⊢ (???(?(??%)?));