Function vstd::seq::axiom_seq_push_len

source · 
pub broadcast proof fn axiom_seq_push_len<A>(s: Seq<A>, a: A)
Expand description
ensures
#[trigger] s.push(a).len() == s.len() + 1,