shorten vtoclgft (#4602)

set.mm

@@ -32797,15 +32797,14 @@ general is seen either by substitution (when the variable ` V ` has no
     vtoclgft $p |- ( ( ( F/_ x A /\ F/ x ps )
                   /\ ( A. x ( x = A -> ( ph <-> ps ) )
                      /\ A. x ph ) /\ A e. V ) -> ps ) $=
-      ( vz wa cv wceq wb wi wal wex wn weq biimp cbv1v alnex syl5ib imp wnf w3a
-      wnfc wcel elisset nfv nfnfc1 nfcvd nfeqd nfnd nfvd eqeq1 a1i notbi syl6ib
-      id syl6 equcomi biimpr syl56 impbid 3bitr3g con4bid ad2antrr 3impia com23
-      imim2i alanimi 19.23t adantl 3adant3 mpd ) CDUCZBCUAZGZCHZDIZABJZKZCLACLG
-      ZDEUDZUBVQCMZBVOVTWAWBVMWAWBKVNVTWAFHZDIZFMZVMWBFDEUEVMWEWBVMWDNZFLZVQNZC
-      LZWENWBNVMWGWIVMWFWHFCVMFUFZCDUGZVMWDCVMCWCDVMCWCUHVMUPUIUJZVMWHFUKZVMFCO
-      ZWFWHJZWFWHKVMWNWDVQJZWOWNWPKVMWCVPDULUMWDVQUNUOZWFWHPUQQVMWHWFCFWKWJWMWL
-      CFOWNVMWOWHWFKCFURWQWFWHUSUTQVAWDFRVQCRVBVCSVDVEVOVTWBBKZWAVOVTWRVTVQBKZC
-      LZVOWRVSAWSCVSAWSVSVQABVRABKVQABPVGVFTVHVNWTWRJVMVQBCVIVJSTVKVL $.
+      ( vz wnfc wnf wa cv wceq wb wi wal wcel wex wn alnex syl5ib imp w3a nfcvd
+      elisset nfv nfnfc1 nfeqd nfnd nfvd weq eqeq1 notbid cbv2w 3bitr3g con4bid
+      a1i ad2antrr 3impia biimp imim2i com23 alanimi 19.23t adantl 3adant3 mpd
+      id ) CDGZBCHZIZCJZDKZABLZMZCNACNIZDEOZUAVKCPZBVIVNVOVPVGVOVPMVHVNVOFJZDKZ
+      FPZVGVPFDEUCVGVSVPVGVRQZFNVKQZCNVSQVPQVGVTWAFCVGFUDCDUEVGVRCVGCVQDVGCVQUB
+      VGVFUFUGVGWAFUHFCUIZVTWALMVGWBVRVKVQVJDUJUKUOULVRFRVKCRUMUNSUPUQVIVNVPBMZ
+      VOVIVNWCVNVKBMZCNZVIWCVMAWDCVMAWDVMVKABVLABMVKABURUSUTTVAVHWEWCLVGVKBCVBV
+      CSTVDVE $.
     $( $j usage 'vtoclgft' avoids 'ax-13'; $)
   $}