Function vstd::seq::axiom_seq_push_index_same

source · 
pub broadcast proof fn axiom_seq_push_index_same<A>(s: Seq<A>, a: A, i: int)
Expand description
requires
i == s.len(),
ensures
#[trigger] s.push(a)[i] == a,