enrich
   list-data
with
   functions 
       . ' : 'a → list('a);
       . + . : list('a) × list('a) → list('a);
       . + . : list('a) × 'a → list('a);
       . +2 . : 'a × 'a → list('a);
       . map . : list('a) × ('a → 'b) → list('b);
       . .foldLeft ( . ) : list('a) × 'b × ('b × 'a → 'b) → 'b;
   
   predicates 
       . ∈ . : 'a × list('a);
   
   variables 
       a : 'a;
       b : 'b;
       x : list('a);
       y : list('a);
       z : list('a);
       f : 'a → 'b;
   
   
   axioms 
      map-base: [] map f = [];
      used for: ls, s;
      
      map-rec: (a ' + x) map f = f(a) + (x map f);
      used for: ls, s;
      
      foldLeft-base: [].foldLeft(b, g) = b;
      used for: ls, s;
      
      foldLeft-rec: (a + x).foldLeft(b, g) = g(x.foldLeft(b, g), a);
      used for: ls, s;
      
      Nil: [] + x = x;
      used for: s, ls;
      
      Cons: (a + x) + y = a + (x + y);
      used for: ls;
      
      One: a ' = a + [];
      
      Last: x + a = x + a ';
      used for: s, ls;
      
      Two: a +2 a0 = a ' + a0 ';
      used for: s, ls;
      
      in-empty: ¬ a ∈ [];
      used for: s, ls;
      
      in-rec: a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x;
      used for: s, ls;
   
   
end enrich