Misc comment edits

changes-set.txt

@@ -27,6 +27,8 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+13-Sep-22 a1tru     trud
+13-Sep-22 trud      mptru
  8-Sep-22 el2v2     elvd        moved from PM's mathbox to main
  8-Sep-22 exlimimdd             moved from ML's mathbox to main
  4-Sep-22 funresfunco           moved from AV's mathbox to main

discouraged

@@ -18946,6 +18946,8 @@ Proof modification of "extwwlkfablem1OLD" is discouraged (257 steps).
 Proof modification of "f1cofveqaeqALT" is discouraged (124 steps).
 Proof modification of "f1oweALT" is discouraged (805 steps).
 Proof modification of "f1rhm0to0ALT" is discouraged (161 steps).
+Proof modification of "falimfal" is discouraged (6 steps).
+Proof modification of "falimtru" is discouraged (6 steps).
 Proof modification of "fnexALT" is discouraged (111 steps).
 Proof modification of "fnmpt2ovdOLD" is discouraged (219 steps).
 Proof modification of "fnotovbOLD" is discouraged (79 steps).
@@ -19783,6 +19785,7 @@ Proof modification of "trsbcVD" is discouraged (398 steps).
 Proof modification of "trsspwALT" is discouraged (64 steps).
 Proof modification of "trsspwALT2" is discouraged (65 steps).
 Proof modification of "trsspwALT3" is discouraged (27 steps).
+Proof modification of "truimtru" is discouraged (6 steps).
 Proof modification of "trujustOLD" is discouraged (21 steps).
 Proof modification of "truniALT" is discouraged (183 steps).
 Proof modification of "truniALTVD" is discouraged (220 steps).

mmnatded.raw.html

@@ -274,7 +274,7 @@
 You can then use the existing assertion Td to prove the resulting conclusion
 with a <tt>T. -&gt;</tt> prefix.
 Finally, you can remove that prefix using
-<A HREF="trud.html">trud</A>, resulting in the conclusion you
+<A HREF="mptru.html">mptru</A>, resulting in the conclusion you
 wanted to prove.</LI>
 
 <LI>To prove some assertion T in closed form,