Improve disjoint variable error message

[tirix]

The error message for missing disjoint variables, Disjoint variable constraint violated, does not mention which constraint is violated, or which additional DV constraint could solve the error.

It would be a nice addition.

$ metamath-knife --verify set.mm
error: Distinct variable violation
      --> set.mm:467384:9
       |
467384 |           qusscaval $p |- ( ( ph /\ K e. S /\ X e. B ) -> ( K .xb [ X ] ( M ~QG G ) ) = [ ( K .x. X ) ] ( M ~QG G ) ) $=
       |  _________^
467385 | |           ( wcel w3a vx cv cqg co cec cmpt cfv cqs csca clmod vv vk vu cvv cqus wceq
467386 | |           a1i cbs eqid ovex qusval quslem wa wbr adantr clss simpr1 eqgvscpbl csubg
467387 | |           wer lsssubg syl2anc eqger syl simpr2 erth lmodvscl syl3anc 3imtr3d eceq1
467388 | |           ecexg ax-mp fvmpt simpr3 eqeq12d 3imtr4d imasvscaval simp3 oveq2d syl3an1
...      |
467404 | |           XCXEURAYLWNWOYTPHFXFDBIKLXFVAONVSWLUCXBWSXEBWTWQXBWRWBWTVAXKXEUPUAIGUEVBXBUP
467405 | |           WRWCWDWEVPWM $.
       | |_________________________^ Disjoint variable constraint violated
       |
1 diagnostics issued.

[jkingdon]

I'd use metamath-exe as the inspiration - it shows the names of the variables both before and after substitution. The output probably could be improved even further, but it would be a place to start.

mmj2 seems capable of something similar (at least in the one quick test I tried) but I guess it only prints a message for the first error.