Function axiom_has_resolved_occupied_entry Copy item path

pub broadcast proof fn axiom_has_resolved_occupied_entry<K, V, A: Allocator>(
    entry: OccupiedEntry<'_, K, V, A>,
)

#[trigger] has_resolved(entry) ==> entry.final_value() == Some(entry.value()),