update todo and clarify unification procedure.
Report correct abstract informations.
Fix App typechecking when x is concrete.
Add type information for alias created by Proj typechecking.
Fix subsorting.
Fix incorect variable substitution.
Fix examples and add a new one with datatype.
Factorize out environment code for eliminators.
Improve unification, following the procedure described in rules.org .