prove abselim_unique

prove abselim_unique

attempting to prove abselim functional

prove abselim t u ==> lamext t u

(i.e. abstraction elimination produces an extensionally equivalent term)
this proof could stand to be substantially shortened by better
automation of lamext convertibility (which maybe I'm just not aware of)

start example of abstraction elimination for lambda terms

One possible use for this is it might help to relate lambda calculus to
combinatory logic (as in examples/ind_def/clTheory). Or it might not.

In any case, what we have here is the start of an attempt to show that
every lambda term is (extensionally) equivalent to a term whose only
abstractions are within occurrences of S and K (considering these
combinators as particular lambda terms).

Have defined the transformation from arbitrary lambda terms to
abstraction-free terms (as a relation) and proved it total. Remains to
show it is functional, and that it produces an equivalent term.