Function teletexstring_fmt 

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

{
    Mapped {
        inner: Refined(
            Tail,
            |bytes: Seq<u8>| {
                is_valid_teletex_string_spec(bytes) && vstd::utf8::valid_utf8(bytes)
            },
        ),
        mapper: (
            |bytes: Seq<u8>| TeletexStringSpec {
                inner: vstd::utf8::decode_utf8(bytes),
            },
            |s: TeletexStringSpec| vstd::utf8::encode_utf8(s.inner),
        ),
    }
}