 The converse of this claim is, obviously, not true. For example, \(\textsf{WI}\) strongly normalizes but untypable, because the antecedent of contraction cannot be unified with any instance of self-implication. The aim to extend the set of typable terms led to the introduction of \(\land\) into types.