 where \(N\) is a term built from basic combinators and \(\alpha\) is structurally isomorphic to A (likewise \(\beta\) to B). That is, one can generate A \(\Rightarrow\) B from A \(\rightarrow\) B by replacing each occurrence of \(\rightarrow\) by \(\Rightarrow\), given a uniform substitution (perhaps the trivial identity one) of sentential letters in the formulae of the propositional language by names for basic types. 