Function defaulted_fmt 

pub open spec fn defaulted_fmt<Field: SpecByteLen, Rest: SpecByteLen, const DER: bool>(
    field: Field,
    default: Field::T,
    rest: Rest,
) -> DefaultedInnerFmt<Field, Rest, Field::T, Rest::T, DER>

{
    Mapped {
        inner: Refined(
            Optional(field, rest),
            |(value, _): (Option<Field::T>, Rest::T)| {
                DER ==> (value matches Some(value) ==> value != default)
            },
        ),
        mapper: (
            |(parsed, rest): (Option<Field::T>, Rest::T)| (
                match parsed {
                    Some(value) => value,
                    None => default,
                },
                rest,
            ),
            |(value, rest): (Field::T, Rest::T)| (
                if value == default { None } else { Some(value) },
                rest,
            ),
        ),
    }
}