{ intro hp 
  have hnp : ¬ p := h_left hp
  contradiction }
case hnp
p : Prop
h_left : p → ¬p
h_right : ¬p → p
⊢ ¬p

case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hnp : ¬p
⊢ False
case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
hnp : ¬p
⊢ False