{ intro hna
  apply False.elim
  apply hna
  exact ha }
case left
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ ¬a → b

case right
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b → b
case right
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b → b