Crunched a few gaps, equality of multiset still missing
Replaced remdups_adj lemma by shorter proof...