Hello @bbb@sbozhko . Today I was in the mood and I started this job. I started with bigcat. Besides adding comments, I also slightly restructured the file to make a better explanation and deflate these big hypotheses, trying to mimic what the style of the wc proof.
