move find_index from compilerLib to miscTheory

so it can be reused in hol-light without introducing a dependency on
compiler-related stuff.
define de Bruijn terms, substitution and instantiation

and try and fail to prove connections back to the analogous operations
on name-carrying terms.