(fmod QID is
  sort Qid .
  ops a e i o u : -> Qid .
endfm)

(fmod LIST is
  pr QID .
  sorts List NeList .
  subsorts Qid < NeList < List .
  op nil : -> List [ctor] .
  op __ : List List -> List [ctor assoc id: nil] .
  op __ : List NeList -> NeList [ctor ditto] .
  op __ : NeList List -> NeList [ctor ditto] .
endfm)

(fmod PALINDROME is
  protecting LIST .
  sorts NePal Pal .
  subsorts Qid < NePal < Pal .
  op nil : -> Pal [ctor] .
  var I : Qid .
  var P : Pal .
  mb I P I : NePal .
endfm)