(VAR x xs ys)

(DATATYPES
   Elem = < >
   L = µX. < nil, cons(Elem,X) >
 )

(SIGNATURES
   append :: L x L -> L
 )

(RULES
  append(nil, ys)      -> ys
  append(cons(x,xs), ys) -> cons(x,append(xs, ys))
 )