Function bytes_eq 

pub exec fn bytes_eq(a: &[u8], b: &[u8]) -> r : bool

ensures

r == (a@ == b@),

r == (a.deep_view() == b.deep_view()),