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