(fmod LIST is
  sort List .
  ops a b c nil : -> List [ctor] .
  op append  : List List -> List [ctor] .
  vars L P Q : List .
  eq append(append(L, P), Q) = append(L, append(P, Q)) .
  eq append(L, nil) = L .
  eq append(nil, L) = L .
endfm)