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 = y is postfix of x;
   
   variables 
       a : A;
       b : A;
       c : A;
       x : List[A];
       y : List[A];
       z : List[A];
       n : Nat;
       m : Nat;
   
   partial functions 
       . last : List[A] → A with λ x. x ≠ [];
       . butlast : List[A] → List[A] with λ x. x ≠ [];
       . dropRight ( . ) : List[A] × Nat → List[A] with λ x, n. 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: x.dropRight(0) = x;
      used for: s, ls;
      
      butlastN-rec: x.dropRight(n + 1) = x.butlast.dropRight(n);
      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 + y = x);
      used for: ls;
   
   
end enrich