[idea] graph-based implementation of lambda calculus

[xieyuheng]

Normal forms of Parigot numerals are exponential in size, but a reasonable term-graph implementation should be able to keep them linear via sharing.

Implement lamping reduction by inet.

After this, we can use lambda encoding for real.

After using lambda encoding for real, maybe we can get better understanding of inductive datatype

For example, parameters v.s. indexes.