zDefine various type inferencer constants

so the definitions using encode/decode aren't added to computeLib
attempt to make compilerTermination add the assumptionless thms to computeLib

I don't know why the ones with assumptions were entered in the first
place though - what does Hol_defn do?
bit of progress on EVALing the repl_fun

Typechecker no longer loops, and we can generate code!

Still need to cheat on the unify stuff to discharge the wfs hypotheses -
it may not be worth doing that properly unless we really need to EVAL
the typechecker.

Now running bc_eval on the generated code loops.