pub open spec fn seq_to_map<V>(s: Seq<V>, off: int) -> IMap<int, V>
{ IMap::new(|i: int| off <= i < off + s.len(), |i: int| s[i - off]) }