Function integer_bytes_wf 

pub open spec fn integer_bytes_wf(bytes: Seq<u8>) -> bool

{
    &&& bytes.len() > 0
    &&& integer_bytes_minimal(bytes)

}