pub broadcast proof fn axiom_seq_add_index1<A>(s1: Seq<A>, s2: Seq<A>, i: int)
0 <= i < s1.len(),
#[trigger] s1.add(s2)[i] == s1[i],