simp[encodeDecode, h]
α✝ : 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
no goals