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