Large quantification

Начинаю прозревать, как понимать proof irrelevant quantification/erasure и large quantification в теории типов. ( Read more... )