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

State before:
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
h : decode e.unpair.1 = none
⊢ encodeDecode ((a : α) × β a) e = none
Tactic:
simp[encodeDecode, h]
State after:
no goals