Refined substituting uninterpreted terms with static variables.
Started adding support for uninterpreted functions in the type checker.