[MetaPRL Users] Term extraction problem

[Wojtek Moczydlowski]

On Tue, 5 Sep 2006, Aleksey Nogin wrote:

> Remember that by default "refine" updates whatever level ("rulebox") you are 
> currently on. You need to either:
> - use "refine lamAbs thenT axiomVar 1" to update the current rulebox to 
> contain the combined step, or
> - use "down 1" (or click on the subgoal number "1") to navigate to the 
> subgoal before applying the axiomVar there.
>
Right, now it works. So back to my original problem, what's the correct way
of extracting lambda x.x out of this proof, if term_of_extract is a hack?

Thanks,

Wojtek