Что-то попытки подключить к Агде унивалентность (отключив аксиому K) приводят к еженедельному обнаружению дырок в паттерн-матчинге. Вот опять сообщают. Следите за рассылкой, оставайтесь на острие.