Десубстификация и деконгофикация

[deniok]

Очень заманчивая идея о том, как в Agda загнать под капот навязчивые subst и cong. Пример от автора.