Rule. conj_elimr
(H ⊢ A ∧ B) → (H ⊢ B)