pub proof fn lemma_disjoint_iff_empty_intersection<T>(a: Set<T>, b: Set<T>)Expand description
ensures
a.disjoint(b) <==> a.intersect(b).is_empty(),Two sets are disjoint iff their intersection is empty