move some EqualityType proofs into compilerSideTheory

not sure if the repl translation works properly now - hoping it will
generate fewer EqualityType and other side conditions... (and that I
didn't accidentally break something)