add fold_equiv_limited, admit another bytes/bits lemma