HomeIsabelle/Phabricator

multiset as equivalence class of permuted lists