Helper function which just tries to rewrite e using the equality r without assigning any
metavariables in the tactic state, and without creating any metavariables which cannot be
discharged by cfg.discharger in the process.
Function which tries to perform the rewrite associated to the equality r : expr × bool (the
bool indicates whether we should flip the equality first), at the position pointed to by
l : expr_lens, by rewriting e : expr. If this succeeds, rewrite_at_lens computes (by unwinding
l) a proof that the entire expression represented by l.fill e is equal to the entire expression
l.fill f, where f is the expr which has replaced e due to the rewrite. It then returns the
singleton list containing this rewrite (and the tracking data needed to reconstruct it directly). If
it fails, it just returns the empty list.