Function axiom_fresh_cursor_id_not_in_dom Copy item path

pub proof fn axiom_fresh_cursor_id_not_in_dom<'rcu>(
    m: Map<CursorId, CursorEntry<'rcu>>,
)

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