Function lemma_value_len_matches_byte_len 

pub broadcast proof fn lemma_value_len_matches_byte_len<C: ValueByteLen + Consistency>(
    c: C,
    v: C::T,
)

requires

c.consistent(v),

ensures

#[trigger] c.byte_len(v) == C::value_byte_len(v),

Broadcast wrapper for ValueByteLen::lemma_value_len_matches_byte_len.