 in which the second step, to the intermediate conclusion B \(\rightarrow\) A, is an instance of \(\rightarrow\)I(ntroduction) with vacuous discharge of the unassumed antecedent B (in a sequent calculus version, the rule of thinning, adding extra assumptions in the sequent antecedent, would be used). The type theoretic proof in type theory  TT[4]  of the construction of a term “inhabiting” the type \(\alpha  \Rightarrow(\beta \Rightarrow \alpha)\) takes the form: 