specification sorts Elem; constants ⊥ : Elem; variables e : Elem; axioms exists-elem: ∃ e. e ≠ ⊥; end specification