Function universalstring_fmt 

pub open spec fn universalstring_fmt() -> Mapped<Refined<Tail, PredFnSpec<Seq<u8>>>, FnSpecMapper<Seq<u8>, Seq<char>>>

{
    Mapped {
        inner: Refined(Tail, |bytes: Seq<u8>| is_valid_universal_string(bytes)),
        mapper: (
            |bytes: Seq<u8>| decode_universal_string(bytes),
            |chars: Seq<char>| encode_universal_string(chars),
        ),
    }
}