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;
       bx : List[B];
       n : Nat;
   
   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