Rule. disj_intror
(H ⊢ B) → (H ⊢ A ∨ B)