cases h with
| inl h₁ => cases h₁ with
            | inl h₃ => exact Or.inl h₃
            | inr h₄ => exact (Or.inr (Or.inl h₄))
| inr h₂ => exact Or.inr (Or.inr h₂)
P Q R : Prop
h : (P ∨ Q) ∨ R
⊢ P ∨ Q ∨ R
no goals