Title: Heq: a Coq library for heterogeneous equality

Abstract:

We give an introduction to the library Heq, which provides a
set of tactics to manipulate heterogeneous equality and explicit
coercion, such as rewriting of heterogeneous equality and
elimination and relocation of explicit coercions.