(fmod LIST-EXAMPLE is sorts Element List . subsorts Element < List . op a : -> Element [ctor] . op b : -> Element [ctor] . op c : -> Element [ctor] . op nil : -> List [ctor] . op _;_ : List List -> List . op _;_ : Element List -> List [ctor] . eq (L:List ; P:List) ; Q:List = L:List ; (P:List ; Q:List) . eq L:List ; nil = L:List . eq nil ; L:List = L:List . endfm)