Function lemma_u64_le_bytes_roundtrip 

pub broadcast proof fn lemma_u64_le_bytes_roundtrip(i: [u8; 8])

ensures

#[trigger] u64_le_to_bytes(u64_le_from_bytes(i)) == i,