prove most of the cheats in exp_to_i4_correct

The one remaining cheat is slightly worrying but should be OK - it's
about lookup of a SOME key being equal in two alists where we know that
the alists are equal when they are filtered down to SOME keys.

The cheats were proved using much nicer tactics for doing this kind of
proof underneath existential quantifiers that is required when we the
relation on values is not plain equality. Hopefully these tactics will
have some reusability in later similar induction proofs. They reduce the
amount of typing of arguments and names (and the requisite
match-abbreviating) to instantiate inductive hypotheses and lemmas in a
way that matches part of the goal under quantifiers.