Discussion: removing sort variables from the internal representation(s)

To avoid the overhead of handling sort variables in all matters of internal terms in the new codebase, we should investigate to what extent we can remove sort variables during internalisation

• The only two symbols that have sort variables are inj and built-in if-then-else
  • We can represent these two symbols with custom nodes in the Term type
  • During internalisation, symbol applications of these symbols are recognised and handled specially.
  • The required sort information should already be available in the KJApp AST node (given we know the two symbols and their sort variable usage).
• Axioms often use sort variables, but it appears as though rewrite rule axioms do not.
  • subsort axioms and functional axioms use a sort variable R for the result sort of \equals
  • equations (simplification axioms) likewise use sort variables R and Q0 for \equals and \in
  • other axiom flavours need to be investigated
    For all of the above, it appears as though sort variables are a technicality, an internal representation would not require them to represent the essence of the respective axiom.
• The only aliases that use sort variables are weakExistsFinally weakAlwaysFinally and allPathGlobally (not used internally)

Start by reading the new internal representation around the Term type and the KJApp AST node, then trace internalisation of inj and built-in if-then-else. Investigate which axiom flavours and aliases still require sort variables. Done means the removable sort-variable handling is identified and a viable representation strategy is agreed for the affected symbols and axioms.