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

Most important common theorem: strongly normalizing → weakly normalizing.

added 1 commit

• fe933ec7 - Apply suggestion to theories/relations.v

Compare with previous version

added 8 commits

• fe933ec7...087e4ccf - 5 commits from branch master
• ff8eccc6 - Add notation `wn` of weakly normalizing terms; and prove some common theorems about it.
• 85fb9ae4 - CHANGELOG.
• 613153f3 - Intuition for decidability of `red` in `wn_sn`.

Compare with previous version

resolved all threads

LGTM!

resolved all threads

mentioned in commit b4ec8641

merged

Merged, and thanks for the feedback!