tactics: being smarter with implicits on apply_lemma
tactics: being smarter with implicits on apply_lemma

We were calling TcUtil.new_implicit_var, which marks the implicit as
Strict, causing it to be fully typechecked when we're checking that it
was solved.

However, we don't need to be that strict: if the implicit was resolved,
then apply_lemma will check that it was solved correctly in order to
prevent a bug like the one on LemmaArgs.fst.

If it was not solved, it is turned into a goal, and will be constructed
correctly by Meta-F*.

Hence, just call new_uvar which will mark it as Allow_untyped, and only
check that it was indeed solved.

A-Manning/FStar,A-Manning/FStar,A-Manning/FStar,FStarLang/FStar,FStarLang/FStar,FStarLang/FStar