Function lemma_star_static_byte_len 

pub broadcast proof fn lemma_star_static_byte_len<A: StaticByteLen>(inner: A, vs: Seq<A::T>)

requires

super::Star(inner).consistent(vs),

ensures

#[trigger] super::Star(inner).byte_len(vs) == vs.len() * A::static_byte_len(),

The byte length of fixed-width elements is their count times their fixed width.