From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 28 Oct 2009 15:00:14 +0000 (+0000)
Subject: Different aliases, better equality inferred.
X-Git-Tag: make_still_working~3239
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=847f57ed13f0b281dc3f2aa84bd89252d1b6a989;p=helm.git

Different aliases, better equality inferred.
---

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 ⊢ (???(?(??%)?));