feat(library/elaborator): do not create trivial constraints of the form 'ctx |- t =:= t'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/printer): include de Bruijn index in the debug printer

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

The elaborator was missing solutions because of the missing condition at is_simple_ho_match.

This commit also adds a new test that exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
checkpoint

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>