Coherence of Strict Equalities in Dependent Type Theories