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