Function axiom_has_resolved_cursor 

pub broadcast proof fn axiom_has_resolved_cursor<Key, Value, A>(
    cursor: CursorMut<'_, Key, Value, A>,
)

ensures

#[trigger] has_resolved(cursor) ==> cursor.final_map() == cursor@.map,

Once the cursor has been dropped, its prophesied map is its current map.