Function lemma_from_to_base128_roundtrip 

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

requires

bytes.len() > 0,

bytes.len() > 1 ==> bytes[0] != 0,

forall |i: int| 0 <= i < bytes.len() ==> bytes[i] < 128,

ensures

nat_to_base128(nat_from_base128(bytes)) == bytes,