X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsets.ma;h=3f5a4feeeceb634c199b7b7c8727c3289f729025;hb=f5e6cad85ff6f10b63622a0348ad65492578022e;hp=07c7884ce7fc35cd153630ad059c181d3cee789d;hpb=74ba7fa3bde7145bbad4c42051a37c7a7e789301;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 07c7884ce..3f5a4feee 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -32,7 +32,7 @@ nqed.
 
 ntheorem subseteq_trans: ∀A.∀S1,S2,S3: Ω \sup A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3.
  #A; #S1; #S2; #S3; #H12; #H23; #x; #H;
- napply (H23 ??); napply (H12 ??); nassumption;
+ napply (H23 …); napply (H12 …); nassumption;
 nqed.
 
 ndefinition overlaps ≝ λA.λU,V:Ω \sup A.∃x:A.x ∈ U ∧ x ∈ V.