Library Coq.Logic.Eqdep
This file axiomatizes the invariance by substitution of reflexive
equality proofs [Streicher93] and exports its consequences, such
as the injectivity of the projection of the dependent pair.
[Streicher93] T. Streicher, Semantical Investigations into
Intensional Type Theory, Habilitationsschrift, LMU München, 1993.
Exported hints