Function vstd::slice::axiom_spec_len

pub broadcast proof fn axiom_spec_len<T>(slice: &[T])

#[trigger] spec_slice_len(slice) == slice@.len(),