Change the way function are represented in the environment.

A function (Lambda, dependent Pi and Sigma) now use a couple (Env,Ident)
as a representation of the normal form of the term.
Implementation of unification over Pi. Checking of Lam.
Improve the exemple.
Fix Incorrect ident generation for cases.
Simplify the interface for environment access, fix and simplify typechecking for Pi and Sigma.
Typing for case and tag. There is some unsolved issue with the case.
Update examples.