[shorten] upcic with funcrcl2

Author: zwang123

set.mm

@@ -835587,19 +835587,18 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
        existence.  (Contributed by Zhi Wang, 16-Sep-2025.) $)
     upcic $p |- ( ph -> X ( ~=c ` D ) Y ) $=
       ( vp vq cv cfv cop co wceq ccic wbr wreu wrex upciclem1 reurex wcel simpl
-      syl wa 3syl ciso eqid cfunc ccat simpll df-br sylib funcrcl 4syl ad2antrr
-      ccid simplrl simprl wral simprr simplrr upciclem2 isisod brcici rexlimddv
-      cco ) APUOUQZLUROTRKURZUSZSKURZQUTUTVAZRSFVBURVCZUORSMUTZAWRUOWTVDWRUOWTV
-      EABDIGKLMNOPQRSTUOUKULUMVFWRUOWTVGVJAWNWTVHZWRVKZVKZOUPUQZLURPTWQUSZWOQUT
-      UTVAZWSUPSRMUTZXCAXFUPXGVDXFUPXGVEAXBVIACDUAHKLMNPOQSRTUPUNUIUJVFXFUPXGVG
-      VLXCXDXGVHZXFVKZVKZDFWNFVMURZRSXKVNZUBXJAKLUSZFJVOUTZVHZFVPVHZJVPVHZVKXPA
-      XBXIVQAKLXNVCZXOUGKLXNVRVSFJXMVTXPXQVIWAZARDVHXBXIUIWBZASDVHXBXIULWBZXJDF
-      FWMURZFWCURZWNXDMXKRSUBUDYBVNZXLYCVNXSXTYAAXAWRXIWDZXCXHXFWEZXJBDEFYBGIJK
-      LMNWNXDOPQRSTUBUCUDUEYDUFAXRXBXIUGWBZXTYAATEVHXBXIUHWBZYEYFAOTWONUTVHXBXI
-      UJWBZAPTWQNUTVHXBXIUMWBZAGUQIUQLUROWPBUQZKURZQUTUTVAIRYKMUTVDGTYLNUTWFBDW
-      FXBXIUKWBXCXHXFWGZAXAWRXIWHZWIXJCDEFYBHUAJKLMNXDWNPOQSRTUBUCUDUEYDUFYGYAX
-      TYHYFYEYJYIAHUQUAUQLURPXECUQZKURZQUTUTVAUASYOMUTVDHTYPNUTWFCDWFXBXIUNWBYN
-      YMWIWJWKWLWL $.
+      syl 3syl ciso eqid cfunc ad2antrr funcrcl2 cco ccid simplrl simprl simprr
+      wa wral simplrr upciclem2 isisod brcici rexlimddv ) APUOUQZLUROTRKURZUSZS
+      KURZQUTUTVAZRSFVBURVCZUORSMUTZAWMUOWOVDWMUOWOVEABDIGKLMNOPQRSTUOUKULUMVFW
+      MUOWOVGVJAWIWOVHZWMWBZWBZOUPUQZLURPTWLUSZWJQUTUTVAZWNUPSRMUTZWRAXAUPXBVDX
+      AUPXBVEAWQVIACDUAHKLMNPOQSRTUPUNUIUJVFXAUPXBVGVKWRWSXBVHZXAWBZWBZDFWIFVLU
+      RZRSXFVMZUBXEFJKLAKLFJVNUTVCWQXDUGVOZVPZARDVHWQXDUIVOZASDVHWQXDULVOZXEDFF
+      VQURZFVRURZWIWSMXFRSUBUDXLVMZXGXMVMXIXJXKAWPWMXDVSZWRXCXAVTZXEBDEFXLGIJKL
+      MNWIWSOPQRSTUBUCUDUEXNUFXHXJXKATEVHWQXDUHVOZXOXPAOTWJNUTVHWQXDUJVOZAPTWLN
+      UTVHWQXDUMVOZAGUQIUQLUROWKBUQZKURZQUTUTVAIRXTMUTVDGTYANUTWCBDWCWQXDUKVOWR
+      XCXAWAZAWPWMXDWDZWEXECDEFXLHUAJKLMNWSWIPOQSRTUBUCUDUEXNUFXHXKXJXQXPXOXSXR
+      AHUQUAUQLURPWTCUQZKURZQUTUTVAUASYDMUTVDHTYENUTWCCDWCWQXDUNVOYCYBWEWFWGWHW
+      H $.
   $}