Hotfix check/adjust subsorting for substitutions based on ==K terms

[jberthold]

When a constraint of shape VAR:VarSort ~> .K ==K term:TermSort ~> .K is externalised, the prior code just rendered a VAR:VarSort #Equals term:TermSort. This is wrong when TermSort /= VarSort, however TermSort will be a subsort of VarSort, otherwise the rule that introduced this ==K term is ill-sorted.

• Externalisation code now inserts the missing injection into the #Equals expression.
• A test was added which demonstrates the use case and behaviour (failed before, succeeds now).
• A pretty-printer option was added to show the injections in the printed terms (off by default).