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