Function axiom_fresh_vm_space_id_not_in_dom Copy item path

pub proof fn axiom_fresh_vm_space_id_not_in_dom<'a>(m: Map<VmSpaceId, VmSpaceOwner>)

!m.dom().contains(fresh_vm_space_id(m)),