(картина "лучшего в мире рисовальщика петухов" "Очень одинокий петух" взята с просторов интернета)

Сопоставление с образцом в Coq на первый взгляд выглядит не сложнее, чем в большинстве языков программирования, т.е. довольно просто. Правда, это впечатление остаётся только до тех пор, пока программисту не приходится столкнуться с зависимыми типами. И тут всё становится гораздо интереснее. Тем не менее интуицию вполне можно выработать. У автора было желание получше разобраться с данной темой и выдалось немного свободного времени. Надеемся, что результат окажется полезен и читателю.