 The decision procedures for \(T_\rightarrow^\textbf{t}\) and \(R_\rightarrow^\textbf{t}\) do not use \(\textrm{TA}_\textrm{CL}\) or axiomatic calculi, instead, they build upon consecution calculi (i.e., sequent calculi in which the structural connective is not assumed to be associative). The idea that there is an affinity between structural rules and combinators goes back at least to Curry (1963). To tighten the connection, Dunn and Meyer (1997) introduced structurally free logics in which introduction rules for combinators replace structural rules—hence the label for these logics. Bimbó and Dunn (2014) introduced a technique to generate a combinatory inhabitant for theorems of \(T_\rightarrow\) from their standard proofs in the sequent calculus, which is used in the decision procedure for \(T_\rightarrow^\textbf{t}\).  Sequent calculi provide better control over proofs than natural deduction or axiomatic systems do. The combinatory extraction procedure of Bimbó and Dunn (2014) yields an effective link between combinators and types grounded in sequent calculus proofs, which obviates the apparent advantage of \(\textrm{TA}_\textrm{CL}\) and axiomatic systems.