Eos3.6 on Mathematica 13.1: problems and tentative solution

So far, our test showed  the following incompatibility wi 13.0:

  1. FoldLine specification may have to change since the solution order may be changed.
  2. 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.