fix(util/buffer): warning produced by clang++

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/elaborator): bug in the elaborator

The elaborator was not handling correctly constraints of the form

    ctx |- ?m << (Pi x : A, B)
    and
    ctx |- (Pi x : A, B) << ?m

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(builtin/kernel): start with small universes

The universe constraint manager is more flexible now.
We don't need to start with a huge universe  U >= 512.
We can start small, and increase it on demand.

If module mod1 needs it, it can always add

   universe U >= 3

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/elaborator): array bounds

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(builtin/cast): remove dominj axiom, it is not consistent with the new semantics of Pi/forall

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(builtin/cast): remove dominj axiom, it is not consistent with the new semantics of Pi/forall