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).
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.