Function bound_as_ref 

pub open spec fn bound_as_ref<T>(b: &Bound<T>) -> Bound<&T>

{
    match b {
        Bound::Included(start) => Bound::Included(start),
        Bound::Excluded(start) => Bound::Excluded(start),
        Bound::Unbounded => Bound::Unbounded,
    }
}