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