MIPT-Coq-24-Lect-10

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: практическое доказывание теорем в логике предикатов; шаблоны в destruct и intros; тактики specialize, apply ... with, enough, classical_left, classical_right; тактикал do.