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

State before:
α : Type u_1
inst✝ : Primcodable α
a : α
⊢ goedelNumber (encode a) = goedelNumber a
Tactic:
simp [Semiterm.Operator.encode, goedelNumber_def]
State after:
no goals