apply And.right
case left
a b : Prop
hab : a ∧ b
⊢ b

case right
a b : Prop
hab : a ∧ b
⊢ a
case left.self
a b : Prop
hab : a ∧ b
⊢ ?left.a ∧ b

case left.a
a b : Prop
hab : a ∧ b
⊢ Prop

case right
a b : Prop
hab : a ∧ b
⊢ a