 the theorem is the typed version of the decidability of the implicational fragment of the logic of ticket entailment \(T_\rightarrow\), that was proved—together with the decidability of \(R_\rightarrow\) (\(R_\rightarrow\) with the truth constant \(t\)) and \(T_\rightarrow^\textbf{t}\) (\(T_\rightarrow\) with the truth constant \(t\))—in Bimbó and Dunn (2012) and Bimbó and Dunn (2013). An independent result (for \(T_\rightarrow\) only) is in Padovani (2013), which extends Broda et al. (2004).