Rule disj_intror

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

Disjunction introduction from the right proposition.