Theorem: LoVe.BackwardProofs.I (LoVe/Labs/Lab2Solution.lean)

State before:
a : Prop
⊢ a → a
Tactic:
intro ha
State after:
a : Prop
ha : a
⊢ a

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