Без заголовка

Что-то в этом роде. К примеру сейчас у меня не получается наскоком решить проблему, и надо лезть в мета-теорию системы Coq и там разбираться по порядку. И почему-то неохота это делать, там сложности всякие. Неосвоенный кусок есть, осваивать лень, наскоком не получается :).