Function lemma_invert_bytes_involutive 

pub proof fn lemma_invert_bytes_involutive(bytes: Seq<u8>)

ensures

invert_bytes(invert_bytes(bytes)) == bytes,