Theorem Set.insert_sdiff_eq_singleton

Modification history