#113 Inconsistencies between ISO-Z and ZEves toolkits

[Leo Freitas]

ISO0Z makes some math toolkit definitions as operator templates like min/max/succ --- for no good reason it seems ----
whereas ZEves doesn't. Hence, when sending/receving traffic between them, some adjustment is needed when the
function is used as an operator. So, if given as "min~S" it's fine both ways, but if as "\dom~min" it isn't. CZT doesn't
parse it and requires it to be "\dom~(min~\_)", whereas ZEves doesn't recognise the operator template for min. Similarly,
when parsing back from the ZEves result, CZT can't make sense of ZEves' answer as "x \in \dom~min". So, at that point
it should be translated from ZEves to CZT as "\dom~(min~\_)". Searching the toolkits, these three cases are the only ones.

Ex:

\begin{theorem}{rule funnyLemma1}
\forall S: \power_1~\num @ \dom~(min~\_) \in \power~S
\end{theorem}
\begin{theorem}{rule funnyLemma2}
\forall S: \finset_1~\num | x \in S @ min~S \in S
\end{theorem}
\begin{zproof}[funnyLemma2]
use explicitMin;
rearrange;
rewrite;
\end{zproof}

[Leo Freitas]

PS:
perhaps add these two theorems and proof as test cases to the ZEves printer as well for doc purposes.