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

[deni_ok]

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