 A combinator that inhabits an implicational theorem encodes a proof of that theorem in the deduction system TA\(_\textrm{CL}\). There is an algorithm to recover the formulas that constitute a proof of the type of the combinator, moreover, the algorithm produces a proof that is minimal and well-structured.  The correspondence between implicational theorems of intuitionistic logic (and their proofs) and typable closed \(\lambda\)-terms (or combinators) is called the Curry–Howard isomorphism. The usual notion of a proof in a Hilbert-style axiomatic system is quite lax, but it can be tidied up to obtain the notion of traversing proofs. In a traversing proof there is a one-one correspondence between subterms of a combinator and the formulas in the traversing proof as well as between applications and detachments therein (cf. Bimbó 2007).