Theorem: LoVe.BackwardProofs.δ_example (LoVe/Lectures/LoVe03_BackwardProofs_Demo.lean)

State before:
⊢ double 5 = 5 + 5
Tactic:
rfl
State after:
no goals