1. The last commit that fixed unification of compound coercions with

1. The last commit that fixed unification of compound coercions with
   applied atomic coercions used to introduce too many compound coercions
   at the end. In this commit we fix the problem in a brutal way by
   mergin coercions every time CicMetaSubst.apply_subst is called.
   To be refined later on.
2. Several bug fixed in coercions handling. In particular, a coercion whose
   source or target was a name was given an invalid URI and was not unified
   and applied correctly.
3. New version of the algebraic library. In this version we differentiate
   between pre-structures and structures. This allows a few theorems/lemmas
   to be stated in a more natural way.