Rules for discharging value-listp hypotheses.
Some symbolic execution rules have hypotheses saying that certain terms are lists of values, i.e. satisfy value-listp. These are discharged by the rules here, in conjunction with the rules in atc-valuep-rules.