enrich
   list
with
   functions 
       . ++ . : List[A] × A → List[A] prio 9 left;
       . distinct : List[A] → List[A];
      comment: removes from the beginning, i.e. the last occurrence of an
                                     element remains in the list.;
   
   predicates 
       dups : List[A];
       disj : List[A] × List[A];
   
   variables 
       a : A;
       b : A;
       c : A;
       x : List[A];
       y : List[A];
       z : List[A];
       bx : List[B];
       f : A → B;
       fa : B;
   
   axioms 
      rmdup-e: [].distinct = [];
      used for: s, ls;
      
      rmdup-y: a ∈ x → (a ' + x).distinct = x.distinct;
      used for: s, ls;
      
      rmdup-n: ¬ a ∈ x → (a ' + x).distinct = a + x.distinct;
      used for: s, ls;
      
      adjoin-in: a ∈ x → x ++ a = x;
      used for: s, ls, lc;
      
      adjoin-notin: ¬ a ∈ x → x ++ a = a + x;
      used for: s, ls;
      
      dups: dups(x) ↔ (∃ a, x0, y, z. x = x0 + (a + (y + (a + z))));
      
      disjoint: disj(x, y) ↔ (∀ a. ¬(a ∈ x ∧ a ∈ y));
   
   
end enrich