Function spec_serialize_seq 

pub open spec fn spec_serialize_seq<A: SpecSerializer>(
    inner: &A,
    vs: Seq<A::SVal>,
) -> Seq<u8>

{ vs.fold_left(Seq::empty(), |buf: Seq<u8>, elem| buf + inner.spec_serialize(elem)) }