Proposition 1.3.1 (Curry-Howard for IPC(->)). Assuming that:

• $\mathrm{\Gamma }$ is a context for $\lambda (\to )$

• $\phi$ a proposition

• (1) If $\mathrm{\Gamma }⊩M:\phi$, then $|\mathrm{\Gamma }|=\{\tau \in \mathrm{\Pi }:(x:\tau )\in \mathrm{\Gamma }\text{ for some }x\}{⊢}_{\text{IPC(}\to \text{)}}\phi$
• (2) If $|\mathrm{\Gamma }|{⊢}_{\text{IPC(}\to \text{)}}\phi$, then there is a simply typed $\lambda$-term $M\in \lambda (\to )$ such that $\{(x_{\psi }:\psi )|\psi \in \mathrm{\Gamma }\}⊩M:\phi$.