Доказательства интуиционистских высказываний через явное выписывание термов, упражнения на зависимый паттерн-матчинг
Introduction to Formal Verification