Constant.v: variants without Funext; cleanups

[jdchristensen]

First commit:

Add variants of cconst_wconst_hset and merely_rec_hset that don't require Funext.

Also clean up some proofs, e.g. the proof of equiv_merely_rec_hset_if_domain. Also factor out hprop_image_wconst_hset_if_merely_domain.

Second commit:

Minor fixes, e.g. drop unneeded backticks, fix indentation, and consistently name the WeaklyConstant argument wc.