Theorem: LoVe.BackwardProofs.Not_Not_intro (LoVe/Lectures/LoVe03_BackwardProofs_Demo.lean)

State before:
a : Prop
⊢ a → ¬¬a
Tactic:
intro ha hna
State after:
a : Prop
ha : a
hna : ¬a
⊢ False

State before:
a : Prop
ha : a
hna : ¬a
⊢ False
Tactic:
apply hna
State after:
a : Prop
ha : a
hna : ¬a
⊢ a

State before:
a : Prop
ha : a
hna : ¬a
⊢ a
Tactic:
exact ha
State after:
no goals