prove splitandpad_equiv (without induction), define several lemmas relating bytes/bits computational/inductive (seem to be true but not proved TODO), and use them