discharge length admits in SHA_equiv, admit InBlocks/length correspondence in sha_padding_lemmas. lengths (multiplication existence, division, inductive) are annoying to deal with