Rules for discharging value-optionp hypotheses.
Some symbolic execution rules have hypotheses saying that
certain terms are optional values, i.e. satisfy value-optionp.
These are discharged by the rules here.
The executable counterpart of value-optionp
takes care of the