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

Most important common theorem: strongly normalizing → weakly normalizing.