{ assumption }
case intro.intro.left
p q r s : Prop
hp : p
hq : q
hr : r
⊢ p

case intro.intro.right
p q r s : Prop
hp : p
hq : q
hr : r
⊢ r
case intro.intro.right
p q r s : Prop
hp : p
hq : q
hr : r
⊢ r