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];
       . forall ( . ) : Set[A] × (A → Bool);
       . exists ( . ) : Set[A] × (A → Bool);
   
   variables 
       s : Set[A];
       a : A;
       b : B;
       f : A → B;
       p : A → Bool;
       m : Nat;
       n : Nat;
   
   axioms 
      forall-base: ∅.forall(p);
      used for: s, ls;
      
      forall-rec: (s ++ a).forall(p) ↔ p(a) ∧ s.forall(p);
      used for: s, ls;
      
      exists-base: ¬ ∅.exists(p);
      used for: s, ls;
      
      exists-rec: (s ++ a).exists(p) ↔ p(a) ∨ s.exists(p);
      used for: s, ls;
      
      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