add BetterMultiPriorityPicker and formal proof