Use projections for refine_state.
Use projections in build_* functions.
Auxiliary lemmas.
Some progress on forward simulation.