Heq: a Coq library for Heterogeneous Equality
Chung-Kil Hur · 2009
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. 1