Theorem: cong (Test/Nat/Cong.lean)

State before:
x y : ℕ
f : ℕ → ℕ
⊢ x = y → f x = f y
Tactic:
simp_all
State after:
no goals