In order to fully reduce a term, we need to be able to reduce redexes
that are not at the top level of the term.
- (II)I ~~> IK ~~> K
+ (II)K ~~> IK ~~> K
That is, we want to be able to first evaluate the redex `II` that is
a proper subpart of the larger term, to produce a new intermediate term