 Solution

Under the Implicational Curry-Howard correspondence, propositions are simple types and assumptions are typed variables. The natural-deduction rulescorrespond respectively to the typing rulesAn assumption $x:A$ corresponds to the variable rule. Induction on a proof converts each rule into the matching typing construction; induction on a typing derivation reverses the process. Thus derivability of an implicational formula from assumptions is equivalent to inhabitation of its corresponding type.