Function axiom_has_resolved_vacant_entry Copy item path

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

#[trigger] has_resolved(entry) ==> entry.final_value() == None::<V>,