We discuss the problem of the or-elimination rule in natural deduction, which does not have the correct form for natural deduction inferences.  It is a research problem to fix this!Don't forget to get in touch with me if you want to do the mini-course over Zoom next month, on normalization.