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

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