Shorten and untrivialize ~gripau-sym.

I didn't think about it at the time, but {ko'a cmima ko'a} is not an
acceptable antecedent for a theorem. The proof is still valid --
shorter, even, due to Metamath shenanigans -- if we build
{ko'e cmima ko'a} instead.

mm/jbobau.mm

@@ -2305,7 +2305,7 @@
 $( {` gripau `} is symmetric.
    (Contributed by la korvo, 15-Jul-2024.) $)
 gripau-sym $p |- ko'a gripau ko'a $=
-  ( sbcmima tsb tss btb id gripauris ) AAAAABCZHDEFG $.
+  ( wk2 sbcmima bb id gripauris ) AABBACDEF $.
 
 $(
 #*#*#