spec exun = sort s op z:s axiom exists! x:s . x=z