enrich
   nat
with
   sorts Set[A];
   constants 
       ∅ : Set[A];
   
   functions 
       . ++ . : Set[A] × A → Set[A] prio 9 left;
       # . : Set[A] → Nat;
   
   predicates 
       . ∈ . : A × Set[A];
       . ⊆ . : Set[A] × Set[A];
   
   variables 
       s : Set[A];
       s0 : Set[A];
       s1 : Set[A];
       s2 : Set[A];
       a : A;
       b : A;
       n : Nat;
   
   induction 
      Set[A] generated by ∅ : Set[A],  . ++ .  : (Set[A] × A → Set[A]);
   
   axioms 
      Extension: s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2);
      used for: ls;
      
      In-empty: ¬ a ∈ ∅;
      used for: s, ls;
      
      In-insert: a ∈ s ++ b ↔ a = b ∨ a ∈ s;
      used for: s, ls;
      
      Size-empty: # ∅ = 0;
      used for: s, ls;
      
      Size-insert: ¬ a ∈ s → #(s ++ a) = # s + 1;
      used for: s, ls;
      
      Subset: s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2);
      used for: ls;
   
   
end enrich