enrich
   list-last, 
   list-getput
with
   functions 
       . -l . : List[A] × A → List[A];
       . -1l . : List[A] × A → List[A];
       . -p . : List[A] × Nat → List[A];
      comment: delete element at position;
       . indexOf ( . ) : List[A] × A → Nat;
      comment: zero based;
       frome : List[A] × A → List[A];
      comment: return list starting with elem;
   
   variables 
       x : List[A];
       y : List[A];
       z : List[A];
       a : A;
       b : A;
       n : Nat;
       m : Nat;
       f : A → B;
   
   partial functions 
       . take ( . ) : List[A] × Nat → List[A] with λ x, n. n ≤ # x;
      comment: return first n elements of list;
       . drop ( . ) : List[A] × Nat → List[A] with λ x, n. n ≤ # x;
      comment: apply .tail n times;
       . takeRight ( . ) : List[A] × Nat → List[A] with λ x, n. n ≤ # x;
      comment: return last n elements of list;
       . sublist ( . ) : List[A] × Nat × Nat → List[A] with λ x, n, m. n + m ≤ # x;
      comment: sublist(offset, length, l) returns sublist from offset with length;
   
   axioms 
      del-e: [] -l a = [];
      used for: s, ls;
      
      del-y: (a ' + x) -l a = x -l a;
      used for: s, ls;
      
      del-n: a ≠ b → (b ' + x) -l a = b ' + (x -l a);
      used for: s, ls;
      
      del1-e: [] -1l a = [];
      used for: s, ls;
      
      del1-y: (a ' + x) -1l a = x;
      used for: s, ls;
      
      del1-n: a ≠ b → (b ' + x) -1l a = b ' + (x -1l a);
      used for: s, ls;
      
      delpos-empty: [] -p n = [];
      used for: s, ls;
      
      delpos-base: (a ' + x) -p 0 = x;
      used for: s, ls;
      
      delpos-rec: (a ' + x) -p (n + 1) = a + (x -p n);
      used for: s, ls;
      
      pos-e: [].indexOf(a) = 0;
      used for: s, ls;
      
      pos-y: (a ' + x).indexOf(a) = 0;
      used for: s, ls;
      
      pos-n: a ≠ b → (b ' + x).indexOf(a) = x.indexOf(a) + 1;
      used for: s, ls, lc;
      
      sublist-def: x.sublist(m, n) = x.drop(m).take(n);
      
      firstN-zero: x.take(0) = [];
      used for: s, ls;
      
      firstN-rec: x.take(n + 1) = x.head + x.tail.take(n);
      used for: ls;
      
      restN-zero: x.drop(0) = x;
      used for: s, ls;
      
      restN-rec: x.drop(n + 1) = x.tail.drop(n);
      used for: ls;
      
      lastN-zero: x.takeRight(0) = [];
      used for: s, ls;
      
      lastN-rec: x.takeRight(n + 1) = x.butlast.takeRight(n) + x.last;
      used for: ls;
      
      fromE-empty: frome([], a) = [];
      used for: s, ls;
      
      fromE-yes: frome(a ' + x, a) = a ' + x;
      used for: s, ls;
      
      fromE-no: a ≠ b → frome(a ' + x, b) = frome(x, b);
      used for: s, ls, lc;
   
   
end enrich