Proofs in context

When reasoning about reasoning one often needs to carry out some proof steps within a different theory and to lift the conclusions back to the original theory. The deductive rules to carry out these steps involve different reflection principles or some other notion of proof in context. Reflection principles have to be carefully restricted in order to avoid paradodex. Such restrictions however. we show that proof in context can replace the most common uses of reflection prionciples. We introduce a generalized rule for proof in context and a convenient notation to express nesting of contexts, which allows us to carry out resanong about reasoning in a safe and natural way.