prove base case of SHA_equiv_pad. took a long time because of typoes (hash_blocks -> hash_block, switched arg order in h_star). now: induction step of SHA_equiv_pad + prove def_eq between the bytes/bits defs!