Доказательства интуиционистских высказываний через явное выписывание термов, упражнения на зависимый паттерн-матчинг
Введение в формальную верификацию программ