MIPT-Coq-26-Lect-02

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: бестиповое лямбда-исчисление; термы и подстановки; редукции; лемма о ромбе, теорема Чёрча-Россера, единственность нормальной формы.