Function normalized_only 

pub open spec fn normalized_only<T>() -> Mapped<Void, FnSpecMapper<Never, T>>

{
    Mapped {
        inner: Void("indefinite-length form is not emitted"),
        mapper: (|_never: Never| arbitrary(), |_value: T| arbitrary()),
    }
}