Function lemma_seq_update_len Copy item path

pub broadcast proof fn lemma_seq_update_len<A>(s: Seq<A>, i: int, a: A)

#[trigger] s.update(i, a).len() == s.len(),