work on a bootstrap lemmas cheat

the one about equality types. this ought to be proved by better
automation in the translator, but maybe it's easier to just prove
manually for now...