feat(kernel/type_checker): add proof_irrelevance support to the is_convertible predicate

This commit is debatable. It seems it is better to have proof irrelevance as an axiom, and keep
the type checker simpler. We don't need proof irrelevance very often. So, it is not clear whether
the extra complication is advantageous. So, this commit was not merged with the master branch.

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