 The theorem is the typed equivalent of the decidability of the implicational fragment of the logic of relevant implication. The decidability of \(R_{\rightarrow}\) was proved by Saul A. Kripke in 1959 together with the decidability of the closely related \(E_{\rightarrow}\) (the implicational fragment of the logic of entailment).