pub broadcast proof fn axiom_spec_btree_map_iter<'a, Key, Value, A: Allocator + Clone>(
m: &'a BTreeMap<Key, Value, A>,
)Expand description
ensures
({
let (pos, v) = #[trigger] spec_btree_map_iter(m)@;
&&& pos == 0int
&&& forall |i: int| 0 <= i < v.len() ==> #[trigger] m@[v[i].0] == v[i].1
&&& increasing_seq(v.map(|idx: int, kv: (Key, Value)| kv.0))
}),