proves_IMP for adding new definitions to context

but haven't proved the cases for using the new definitions - just that
they don't mess up previous proofs.