This is a formalization of the book "Type Theory and Formal Proof: An Introduction" by Rob Nederpelt and Herman Geuvers. module README where import Untyped import STLC import SystemF