Describir: The Justification of Identity Elimination in Martin-Löf's Type Theory.