Abstract occurrences of
e. We detect subterms equivalent to
p using key-matching.
That is, only perform
isDefEq tests when the head symbol of substerm is equivalent to head symbol of
By default, all occurrences are abstracted,
but this behavior can be controlled using the
All matches of
e are considered for occurrences,
but at the first match (whether included in the occurrences or not)
metavariables appearing in
e) may become instantiated,
affecting the possibility of subsequent matches.