|- A   |-B
-----------
... |-  A&B      C |- C                                 D |- D
------------------------              ------------------------------
(A & B) => C, A,B,D |- C              (A & B) => C, A,B,D |- D | F
-----------------------------------------
(A & B) => C, A,B,D |- (C & (D | F))




ImpL((A & B) => C, Init, OrR(Init))




              A |- A             C |- C
-------------------------      -------------
(A | B) => C, A |- A | B        C |- (C | D)    
--------------------------------------------------
(A | B) => C, A |- (C | D)



ImpL(A|B=>C, OrR1(Init), OrR2(Init))