Introduction: reuse lsymbols and axioms wherever possible

For programs with a high number of individual sub-VCs after the first split, introduce_premises provoked high memory usage, by generated distinct set of premises for each sub-task.

This commit adds memoization tables to Introduction, allowing to reuse lsymbols and axiom declarations. It relies on the fact that variable binding does not change the bound variable, and uses the idents of these variables to recognize "the same" quantifiers in the sub-tasks produced by split_goal.