stated some lemmas I think I'll need; started proving weakening properties
finished proving weakening for target type judgment
proved t_context_typing_implies_t_context, including definition bugfixes