История изменений
Исправление AndreyKl, (текущая версия) :
что то мне подсказывает что вот это похоже на то что нужно
https://stackoverflow.com/questions/49628762/lifting-generalization
техника похожа на ту что используется для определения гетерогенных списков, но сложнее. Хороший пример, ёлки. Я правда лучше попробую изобразить на идрисе.
Исходная версия AndreyKl, :
что то мне подсказывает что вот это похоже на то что нужно
https://stackoverflow.com/questions/49628762/lifting-generalization
техника похожа на ту что используется для определения гетерогенных списков, но я лучше попробую изобразить на идрисе, ради любопытства.