pub broadcast proof fn axiom_imap_index_decreases_infinite<K, V>(m: IMap<K, V>, key: K)Expand description
requires
m.dom().contains(key),#[trigger] is_smaller_than_recursive_function_field(m[key], m),