[MetaPRL Users] Term extraction problem

[Aleksey Nogin]

On 05.09.2006 11:26, Wojtek Moczydlowski wrote:

> 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?

Well, term_of_extract is not a hack, it's just a low-level function that 
requires some knowledge in order to use properly for derived rules with 
assumptions. In examples like yours, where the rule does not have any 
assumptions, simple "term_of_extract []" should be good enough (as long 
as you do not mind some variables being named "" - an empty string ;-) ).