1. finish formalising [CombinatorialVickreyAuction.thy](/formare/auctions/blob/master/isabelle/Auction/CombinatorialVickreyAuction.thy) and its dependencies 2. revisit the general code for combinatorial static auctions; make sure that it sufficiently abstracts from the specific nVCG situation. 3. revisit the general code for single-good static auctions - as a first step, remove `sga_` prefix from names 4. make (2) and (3) special cases of a more general "static auction" definition