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),
            |pair: (Option<Field::T>, Rest::T)| {
                DER ==> (pair matches (Some(value), _) ==> value != default)
            },
        ),
        mapper: (
            |parsed: (Option<Field::T>, Rest::T)| (
                match parsed.0 {
                    Some(value) => value,
                    None => default,
                },
                parsed.1,
            ),
            |value: (Field::T, Rest::T)| (
                if value.0 == default { None } else { Some(value.0) },
                value.1,
            ),
        ),
    }
}