This episode explains the idea of normalization of proofs in natural deduction. We want to eliminate so-called detours in proofs, which occur when an introduction is immediately followed by an elimination.
See All 179 Episodes of "Iowa Type Theory Commute"