Инъективность и дизъюнктность конструкторов. Большая элиминация. Паттерн "конвой". Доказательства по индукции. Prop и Type.
Introduction to Formal Verification