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