cases h₁ with
| inl nap => cases h₂ with
             | inl ap => exact False.elim (nap ap)
             | inr cp => exact (Or.inr cp)
| inr bp => exact (Or.inl bp)
A B C : Prop
h₁ : ¬A ∨ B
h₂ : A ∨ C
⊢ B ∨ C
no goals