Normalization of detours for implication inferences

We talk about normalizing detours -- which are when an introduction inference is immediately followed by an elimination inference -- for the implication rules. Under Curry-Howard, this actually corresponds to beta-reduction, and could make the proof bigger (though less complex in a certain sense).