Function axiom_slice_decreases_to_seq 

pub broadcast proof fn axiom_slice_decreases_to_seq<T>(s: &[T])

ensures

#[trigger] (decreases_to!(s => s @)),

We axiomatize that a slice can decrease to its corresponding sequence.