eliminate hpq with hp hq
case intro.intro
p q r s : Prop
hpq : p ∨ q
hpr : p → r
hqs : q → s
⊢ r ∨ s
case intro.intro.inl
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
⊢ r ∨ s

case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
⊢ r ∨ s