Theorems for universal property

changes-set.txt

@@ -105,6 +105,7 @@ Date      Old       New         Notes
 16-Sep-25 ismhp     [same]      Removed unneeded hypotheses
 16-Sep-25 selvval   [same]      Removed unneeded hypotheses
 16-Sep-25 mplelsfi  [same]      Removed unused hypothesis
+16-Sep-25 reueqdv   [same]      Moved from GG's mathbox to main set.mm
 11-Sep-25 cascl     [same]      revised - algSc may be non-injective
 10-Sep-25 soeq12d   [same]      Moved from SO's mathbox to main set.mm
 10-Sep-25 freq12d   [same]      Moved from SO's mathbox to main set.mm

discouraged

@@ -14678,6 +14678,7 @@ New usage of "anmp" is discouraged (11 uses).
 New usage of "aprilfools2025" is discouraged (0 uses).
 New usage of "archnq" is discouraged (1 uses).
 New usage of "arglem1N" is discouraged (0 uses).
+New usage of "asclelbasALT" is discouraged (0 uses).
 New usage of "atabs2i" is discouraged (1 uses).
 New usage of "atabsi" is discouraged (1 uses).
 New usage of "atbtwnexOLDN" is discouraged (0 uses).
@@ -19991,6 +19992,7 @@ Proof modification of "anabss7p1" is discouraged (5 steps).
 Proof modification of "ancomstVD" is discouraged (22 steps).
 Proof modification of "anmp" is discouraged (8 steps).
 Proof modification of "aprilfools2025" is discouraged (116 steps).
+Proof modification of "asclelbasALT" is discouraged (84 steps).
 Proof modification of "avril1" is discouraged (194 steps).
 Proof modification of "ax1" is discouraged (3 steps).
 Proof modification of "ax10fromc7" is discouraged (50 steps).