deep optimization : use local theorems for proof steps, added pose steps for local defs

[fredokun]

This is a huge improvement of the LaTTe kernel. The only drawback is the introduction of a new pose construct for making local definitions in proofs. The good point is that this probably increases the readability of the proofs. The sets and integers libraries have been updated.