Fix the translator?

Following Magnnus' suggestion I might have fixed the translator for the
new equality.  I don't fully understand the code I added, but it's very
similar to code that was there before.  The std_prelude and Okasaki
examples don't have eny errors in proving EqualityTypes (but the Okasaki
examples still don't complete).  Haven't tested the repl because of
other broken things on this branch.