simp[encodeDecode]
α : Type u_1
inst✝ : Encodable α
e : ℕ
⊢ encodeDecode α e = Option.map encode (decode e)
α : Type u_1
inst✝ : Encodable α
e : ℕ
⊢ (encode (decode e)).predO = Option.map encode (decode e)