Extend 'apppears_free_in' definition for naturals, and 'prove' context_invariance and free_in_context lemmas