spec stackstuff = sort s; free types stack::=empty|push(top:?s;pop:?stack) pred contains (x:s;a:stack)<=>not a=empty /\ (x=top(a) \/ contains (x,pop(a)))