Rule disj_introl

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

Disjunction introduction from the left proposition.