Refactor/generalize some pipeline definitions/proofs

When we do rewriting after casts, we will need to do extra passes of DCE
and subst01 to fully reduce things, so we generalize some of the interp
proofs over cast behavior.

For ease of rewriting, we make [ident.interp] an alias (notation) for
[ident.gen_interp], rather than a [Definition].

We also factor out the rewriting wrapper inside the pipeline module into
its own definition.

0 files changed, 0 insertions, 0 deletions