{ intro ha
  assumption }
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
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ ¬a → a