pub proof fn lemma_finite_int_set_has_unused(s: Set<int>)Expand description
ensures
exists |id: int| !s.contains(id),A finite Set<int> cannot contain every integer: there always exists
an int outside the set. Used to prove the freshness axioms.