Adding a convenience lemma to avoid breaking the typeof_env abstraction.
generalizing to support an arbitrary equivalence relation on terms

- this is necessary to do unification modulo conversion.
Merge branch 'master' of github.com:gmalecha/mirror-core