BROADCASTS.com

b'

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