rework reader treatment of axioms again

make the reader do all the work of proving the requested axiom (although
one can just use ASSUME if necessary)
some missing vsubst_inst_rws