 Here \(\lambda\) abstraction, the introduction of \(\lambda\) terms, corresponds to \(\rightarrow\)I, so the \(\lambda\) term \(\lambda xy.x\) which is shown to have type \(\alpha \Rightarrow  (\beta \Rightarrow \alpha)\) ‘codes’ two steps of the type correlate of \(\rightarrow\)I, namely the rule \(\Rightarrow\)I introducing function types, and we can recover the above proof of the propositional theorem. Moreover given the tight connection between type theoretical calculi and programs in certain types of programming languages, we can also see the TT proof as a program of steps in the construction of a certain type of computational object.