A "lens" for looking into the subterms of an expression, tracking where we've been, so that
when we "zoom out" after making a change we know exactly which order of
congr_args we need to make things work.
This file is for non-tactics.
expr, expr_lens, congr, environment, meta, metaprogramming, tactic
This type is used in the development of rewriting tactics such as