pub broadcast proof fn axiom_slice_ext_equal<T>(a1: &[T], a2: &[T])
Expand description
ensures
#[trigger] (a1 =~= a2)
<==> (a1.len() == a2.len() && forall |i: int| 0 <= i < a1.len() ==> a1[i] == a2[i]),