So far, our test showed the following incompatibility wi 13.0:
- FoldLine specification may have to change since the solution order may be changed.
- During the writing of ProofDoc, Mathematica system 13.1 may clash.
In the case of 1, change FoldLine in the HO to the appropriate case number.
In the case of 2, the best solution is to split the goal into smaller ones and try each with Prove command.