fmod LIST{X :: TRIV} is
  sorts List NeList .
  subsorts X$Elt < NeList < List .

  op nil : -> List .
  op _ _ : List List -> List [assoc prec 9] .
  op _ _ : NeList List -> NeList [assoc prec 9] .
  op head _ : NeList -> X$Elt .
  op tail _ : NeList -> List .
  op empty? _ : List -> Bool .

  var X : X$Elt .
  var L : List .
  eq head(X L) = X .
  eq tail(X L) = L .
  eq empty? L = L == nil .
endfm

*** Example usage
red head(X nil) .
red tail(X nil) .
red empty?(nil) .
red empty?(head(X nil)) .
red empty?(tail(X nil)) .