Start on proving proof-theoretic conservativity of definitions

So far, just an easy warm-up proving that if something is provable
before an extension of the context, it is still provable afterward
(i.e., the easy direction).