enrich
   list-dup
with
   functions 
       rev : list('a) → list('a);
       mklist : 'a × nat → list('a);
      comment: mklist(a, n), return list with n times a.;
       fillfirst : nat × 'a × list('a) → list('a);
   
   predicates 
       . ⊑ . : list('a) × list('a);
      comment: x ⊑ y = x is prefix of y;
       . ⊒ . : list('a) × list('a);
      comment: x ⊒ y = x is postfix of y;
   
   variables 
       a : 'a;
       b : 'a;
       c : 'a;
       x : list('a);
       y : list('a);
       z : list('a);
       n : nat;
   
   partial functions 
       . .last : list('a) → 'a with λ x. x ≠ [];
       . .butlast : list('a) → list('a) with λ x. x ≠ [];
       butlastn : nat × list('a) → list('a) with λ n, x. n ≤ # x;
      comment: return list except last n elements;
   
   
   axioms 
      butlast-one: a '.butlast = [];
      used for: s, ls;
      
      last-one: a '.last = a;
      used for: s, ls;
      
      butlast-rec: (a ' + b ' + x).butlast = a ' + (b ' + x).butlast;
      used for: s, ls;
      
      last-rec: (b ' + a ' + x).last = (a ' + x).last;
      used for: s, ls;
      
      rev-e: rev([]) = [];
      used for: s, ls;
      
      rev-r: rev(a ' + x) = rev(x) + a;
      used for: s, ls;
      
      mk-zero: mklist(a, 0) = [];
      used for: s, ls;
      
      mk-succ: mklist(a, n + 1) = a ' + mklist(a, n);
      
      butlastN-base: butlastn(0, x) = x;
      used for: s, ls;
      
      butlastN-rec: butlastn(n + 1, x) = butlastn(n, x.butlast);
      used for: s, ls;
      
      fillfirst-longer: n ≤ # x → fillfirst(n, a, x) = x;
      used for: s, ls;
      
      fillfirst-fill: # x < n → fillfirst(n, a, x) = mklist(a, n - # x) + x;
      
      prefix: x ⊑ y ↔ (∃ z. x + z = y);
      used for: ls;
      
      postfix: x ⊒ y ↔ (∃ z. z + x = y);
      used for: ls;
   
   
end enrich