Add notation `wn` of weakly normalizing terms; and prove some common theorems about it.

Merged Robbert Krebbers requested to merge robbert/wn into master

Most important common theorem: strongly normalizing → weakly normalizing.

Merge request reports