Полиморфные функции, зависимые функции, тип-произведение, тип-сумма, неявные аргументы, нотации
Introduction to Formal Verification