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

State before:
h : ∀ (n : ℕ), f n = n
⊢ f 5 = 5
Tactic:
exact h 5
State after:
no goals