Function non_tail_fmt_dps 

pub open spec fn non_tail_fmt_dps<T>(
    serializer_dps: SerializerDPSFnSpec<T>,
    byte_len: ByteLenFnSpec<T>,
) -> bool

{
    &&& forall |v: T, obuf: Seq<u8>| {
        #[trigger] serializer_dps(v, obuf).len() - obuf.len() == byte_len(v)
    }
    &&& forall |v: T, obuf: Seq<u8>| {
        #[trigger] serializer_dps(v, obuf)
            == (choose |w: Seq<u8>| serializer_dps(v, obuf) == w + obuf) + obuf
    }

}

Functional version of NonTailFmt for DPS serializer functions.