identify steps (induction on msg -> need to prove equiv with msg = [] -> 3 equiv lemmas (++, xor, and SHA). + SHA: hash_blocks_equation instead of hash_blocks_terminate