return a lazy list of (t, n, k) where

• t is a tracked_rewrite (i.e. a pair (e' : expr, prf : e = e'))
• n is the index of the rule r used from rs, and
• k is the index of t in all_rewrites r e.

perform_nth_write n rules performs only the nth possible rewrite using the rules.

The core rewrite has a occs configuration setting intended to achieve a similar purpose, but this doesn't really work. (If a rule matches twice, but with different values of arguments, the second match will not be identified.)

As for perform_nth_rewrite, but only working on the left hand side.

As for perform_nth_rewrite, but only working on the right hand side.