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

State before:
a : Prop
⊢ a → ¬¬a
Tactic:
rw [Not]
State after:
a : Prop
⊢ a → ¬a → False

State before:
a : Prop
⊢ a → ¬a → False
Tactic:
rw [Not]
State after:
a : Prop
⊢ a → (a → False) → False

State before:
a : Prop
⊢ a → (a → False) → False
Tactic:
intro ha
State after:
a : Prop
ha : a
⊢ (a → False) → False

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

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

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