More napply \ldots => napply

[helm.git] / helm / software / matita / nlibrary / sets / sets.ma

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index a12f1fc5c52dbc0a89b2ae6096b3e674080f79f9..eb99ee4c5c22595075b5dae056155cacb7d856ca 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -15,8 +15,6 @@
 include "logic/equality.ma".
 
 nrecord powerset (A: Type) : Type[1] ≝ { mem: A → CProp }.
-(* This is a projection! *)
-ndefinition mem ≝ λA.λr:powerset A.match r with [mk_powerset f ⇒ f].
 
 interpretation "powerset" 'powerset A = (powerset A).
 
@@ -34,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.