Построение инстансов типа с разрешимым равенством. Метапрограммирование с каноническими структурами
Introduction to Formal Verification