Function lemma_i64_be_value_roundtrip 

pub broadcast proof fn lemma_i64_be_value_roundtrip(o: i64)

ensures

#[trigger] i64_be_from_bytes(i64_be_to_bytes(o)) == o,