perf: do not revisit shared subterms without matches in `kabstract`

This PR makes `rw` and other tactics based on `kabstract` faster on goals with shared subterms.

`kabstract` traverses its input as a tree, so a shared subterm is visited, and its `isDefEq` candidates are tested, once per occurrence. It now remembers the subterms whose traversal found no match, and skips them when they occur again. The cache is cleared whenever a match is abstracted, since this is the only point where the metavariable context changes. Subterms containing matches that are not abstracted are not cached, so occurrence numbering for `occs` is unchanged.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>