Prove encode_unify (remove last cheat from unifyScript.sml)

The difficulty was that unify sometimes operates on terms for which
there is no encoding (e.g. when it descends into a tagged construct, at
some point it has to unify two tags, neither of which are valid encoded
terms on their own). So the inductive hypothesis needed to be
strengthened significantly to allow for these cases.