Introduce terms and lemmas based on context

[siddhartha-gadgil]

• This is meant for stuff predicted by LLMs.
• In the case of Lemmas, the predicted context may be part of the statement, so we should fold $\forall$'s with variables in the context.
• In general, we should drop matched part of the context, in particular checking if all the context is present.
• We use let and using to introduce, but after checking to avoid duplication.