Changed types in combinatorial auctions according to what suggested by soundness proof in g.thy. Also extended t.thy to multiple participants