PRED-DEFN ::= pred-defn PRED-NAME PRED-HEAD FORMULA PRED-HEAD ::= pred-head ARG-DECL*
A definition PRED-DEFN of a predicate with some arguments is written:
p (V11, ..., V1m1:s1; ...; Vn1, ..., Vnmn:sn) <=> FWhen the list of arguments is empty, the definition is simply written:
p <=> FThe sign displayed as a double-headed double arrow in LaTeX is input as `<=>'.
It declares the predicate name p as a predicate, with a profile having argument sorts s1 (m1 times), ..., sn (mn times). It also asserts the equivalence:
p(V11, ..., Vnmn) <=> Funiversally quantified over the declared argument variables [CHANGED:] (which must be distinct, and are the only ones allowed in T), or just `p <=> F' when the list of arguments is empty.  The predicate name p may occur in the formula F, and may have any interpretation satisfying the equivalence.