Theorem: Encodable.encodeDecode_of_some (Logic/Vorspiel/Computability.lean)

State before:
α : Type u_1
inst✝ : Encodable α
e : ℕ
a : α
h : decode e = some a
⊢ encodeDecode α e = some (encode a)
Tactic:
simp[encodeDecode, h]
State after:
no goals