Improved handling of meta-level auxiliary functions in deduction rules.

Added some explicit classes for binary and ternary meta-level functions.