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