X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsets.ma;h=d4a13507c79bf6790b4d8dce4da16266dc8fb9cc;hb=e91eb82d2b5e032907758bff0b474d62d57463dc;hp=780dc2b4caa7524493c75c78bc0db9a331171246;hpb=ee83e268c87c75161da0e216d87e806effca7bb4;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 780dc2b4c..d4a13507c 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -52,8 +52,8 @@ ndefinition seteq: ∀A. equivalence_relation1 (Ω^A).
  #A; @
   [ napply (λS,S'. S ⊆ S' ∧ S' ⊆ S)
   | /2/
-  | #S; #S'; *; /2/
-  | #S; #T; #U; *; #H1; #H2; *; /3/]
+  | #S; #S'; *; /3/
+  | #S; #T; #U; *; #H1; #H2; *; /4/]
 nqed.
 
 include "sets/setoids1.ma".
@@ -140,7 +140,7 @@ unification hint 0 ≔  A:setoid, x, S;
 nlemma subseteq_is_morph: ∀A. unary_morphism1 (ext_powerclass_setoid A)
  (unary_morphism1_setoid1 (ext_powerclass_setoid A) CPROP).
  #A; napply (mk_binary_morphism1 … (λS,S':𝛀^A. S ⊆ S'));
- #a; #a'; #b; #b'; *; #H1; #H2; *; /4/.
+ #a; #a'; #b; #b'; *; #H1; #H2; *; /5/.
 nqed.
 
 unification hint 0 ≔ A,a,a'