We discuss the problem of the or-elimination rule in natural deduction, which does not have the correct form for natural deduction inferences.\xa0 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.\xa0\xa0