have hnp : ¬ p
case intro
p : Prop
h_left : p → ¬p
h_right : ¬p → p
⊢ False
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