 A famous example of a pair of formulas that have no common instance is \(A\rightarrow A\) and \(A\rightarrow A\rightarrow B\). The instances \(p \rightarrow p\) and \(q\rightarrow q\rightarrow r\) share no propositional variables, however, neither \(q\rightarrow q\) nor \((q\rightarrow r)\rightarrow q\rightarrow r\) matches the shape of the second formula. To put the problem differently, \(q\) and \(q\rightarrow r\) would have to be unified, but they cannot be unified no matter what formula is substituted for \(q\). An immediate consequence of this is that \(\textsf{WI}\) is not typable.