@user21820 @Wojowu @Deedlit @amWhy: I'm going to win myself:
repl.it/Fomr/2. Don't know why I didn't compress the duplicate strings. I look forward to someone helping me to analyze this. The idea came from my proof of the Hydra game termination, where I used a strong third-order lemma labelled as "Exercise" in my code. I thought it was a waste to only use it as many times as the starting tree was deep, so I allowed downward extension, but it took me a while to find the proof.