Theorem: LO.FirstOrder.Arith.FirstIncompleteness.natCast_nat (Logic/FirstOrder/Arith/Representation.lean)

State before:
n : ℕ
⊢ ↑n = n
Tactic:
rfl
State after:
no goals