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

State before:
⊢ (let n := 2;
    n + n) =
    4
Tactic:
rfl
State after:
no goals