MIPT-Coq-CyPr-23-Lect-11

Основы инженерии доказательств (Coq) в МФТИ. Темы: представление кванторов существования и подмножеств с помощью индуктивных типов; индуктивные определения предикатов; тактика exists.