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.