 The correspondence expressed by the previous two theorems between intuitionistic validity and typability is known as the Curry-Howard-de Bruijn correspondence, after three logicians who noticed it independently. The correspondence, as stated, is between only propositional intuitionistic logic, restricted to the fragment containing only the implication connective \(\rightarrow\). One can extend the correspondence to other connectives and to quantifiers, too, but the most crisp correspondence is at the level of the implication-only fragment. For details, see (Howard, 1980).