  If rule  ⊃I is followed by ⊃E,  there is a non-normality that  is removed by a detour conversion: a derivation of B (and  what follows after it) is constructed by taking the derivation of the minor premiss A of the elimination rule and the derivation  of B from the assumption A in the introduction.  These two pieces are combined together into a derivation of  B that does not have the detour formula  A ⊃ B. In Gentzen's thesis, all assumptions are  in the end closed by implication introductions, but nowadays one  considers also derivations that leave a collection of formulas as  open assumptions.