new, with lemma setsum_restrict_fun_zero (needed for CombinatorialVickreyAuctionSoundness.remaining_value_alt)
moved eval_rel_or to RelationOperators; new lemma eval_runiq_rel_or in RelationProperties
further work on lemma remaining_value_alt