enrich
   set-basic
with
   functions 
       { . } : 'a → Set('a);
       . ∪ . : Set('a) × Set('a) → Set('a);
       . ∩ . : Set('a) × Set('a) → Set('a);
       . \ . : Set('a) × Set('a) → Set('a);
       . -- . : Set('a) × 'a → Set('a) prio 9 left;
       . .map ( . ) : Set('a) × ('a → 'b) → Set('b);
       . .filter ( . ) : Set('a) × ('a → Bool) → Set('a);
   
   predicates 
       disjoint : Set('a) × Set('a);
   
   variables 
       s : Set('a);
       a : 'a;
       b : 'b;
       f : 'a → 'b;
       p : 'a → Bool;
       m : Nat;
       n : Nat;
   
   
   axioms 
      filter-in: a ∈ s.filter(p) ↔ a ∈ s ∧ p(a);
      used for: s, ls;
      
      map-base: ∅.map(f) = ∅;
      used for: s, ls;
      
      map-rec: ¬ a ∈ s → (s ++ a).map(f) = s.map(f) ++ f(a);
      used for: s, ls;
      
      One: {a}  = ∅ ++ a;
      used for: ls;
      
      Union: a ∈ s1 ∪ s2 ↔ a ∈ s1 ∨ a ∈ s2;
      used for: s, ls;
      
      Intersect: a ∈ s1 ∩ s2 ↔ a ∈ s1 ∧ a ∈ s2;
      used for: s, ls;
      
      Difference: a ∈ s1 \ s2 ↔ a ∈ s1 ∧ ¬ a ∈ s2;
      used for: s, ls;
      
      Delete: a ∈ s -- a0 ↔ a ≠ a0 ∧ a ∈ s;
      used for: s, ls;
      
      Disjoint: s1 ∩ s2 = ∅ ↔ disjoint(s1, s2);
      used for: s, ls;
   
   
end enrich