apply Or.elim (hem a)
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ a
case left
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ a → a

case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ ¬a → a