Recording a Finite Domain

fof(fi_name, fi_domain
    ! [X] : ( X = e₁ | X = e₂ | ... | X = e_n ).

• e_is are all "distinct object"s, or all distinct integers, or all distinct constant terms.

• "Distinct object"s and distinct integers in signature must be in domain
• "Distinct object"s and distinct integers are already unequal
• Inequality of constant terms must be axiomatized