cases h₁ with
| inl ap => cases h₂ with
            | inl nap => 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