Recording Interpretations of Functors and Predicates

fof(fi_name, fi_functors
    ( f(e₁, ... ,e_m) = e_r
    & f(e₁, ... ,e_p) = e_s
      ... ) ).

• f(e₁, ... ,e_m) is interpreted as e_r, etc
• "Distinct object"s and integers are automatically interpreted as themselves

fof(fi_name, fi_predicates
    ( p(e₁, ... ,e_m)
    & ~ p(e₁, ... ,e_p)
      ... ) ).

• p(e₁, ... ,e_m) is interpreted as true
• p(e₁, ... ,e_p) is interpreted as false
• Equality is interpreted naturally by the domain