Logic normalization transforms predicates and terms from the original
code. Currently the assertion string that is shown to the user when the
assertion fails shows these transformed forms. This should not be the
case, as the user cannot understand where they stem from.

Therefore we need to determine the original forms and use them when
generating the assertion strings.

This commit extends the memoization modules in Logic_normalizer to be
bidirectional maps, such that the original form of a term or predicate
can be determined.