Function vstd::std_specs::vec::ex_vec_insertCopy item path

pub exec fn ex_vec_insert<T, A: Allocator>(vec: &mut Vec<T, A>, i: usize, element: T)

i <= old(vec).len(),

vec@ == old(vec)@.insert(i as int, element),