 are substitution instances of \(p\rightarrow p\) and of \(q\rightarrow q\). Furthermore, all simple types are substitution instances of a propositional variable, hence \(\textsf{II}\) can be assigned both the type \(r\rightarrow r\) and the type (\(s\rightarrow s)\rightarrow s\rightarrow s\)—and, of course, the latter happens to be an instance of  the former because \(A\rightarrow A\) is the principal type schema of \(\textsf{II}\). If we apply condensed detachment to \(p\rightarrow p\) and \(q\rightarrow q\), then we get \(q\rightarrow q\) (via the substitutions \([p/q\rightarrow q]\) and \([q/q])\), and so condensed detachment yields the principal type of \(\textsf{II}\). Incidentally, \(\textsf{II}\) and  \(\textsf{I}\) provide an excellent example to illustrate that distinct terms may have the same principal type schema.