Function lemma_i8_seq_roundtrip 

pub broadcast proof fn lemma_i8_seq_roundtrip(i: Seq<u8>)

requires

i.len() == 1,

ensures

seq![(#[trigger] (i[0] as i8) as u8)] == i,