Function axiom_spec_len Copy item path

pub broadcast proof fn axiom_spec_len<T, A: Allocator>(v: &Vec<T, A>)

#[trigger] spec_vec_len(v) == v@.len(),