Split prettification from proof mode reduction
With this, pm_reduce
just reduces away proof mode terms using cbv
; pm_prettify
just prettifies user-visible connectors using cbn
. Most uses of pm_default
are converted to default
to keep the desired reduction behavior.