4v-sexpr: fill out the sexpr-rewrites a bit more