induction: doesn't work for sha equiv. (TODO) almost works for main theorem (no induction, just lemmas), but we have sha_splitandpad m = M! did this come from my various rewrites or from the original spec?