Что за волшебное слово refl в Agda? Смотрю, как чел доказывает свойства всякие, пишет свойство в типе, а на уровне терма просто refl и всё. Ответ: доказано
Конструктор для пропозиционального равенства, когда его матчишь, система понимает, где чё равно и упрощает