simp[encodeDecode]
α : Type u_1
inst✝ : Encodable α
e i : ℕ
⊢ encodeDecode α e = some i → ∃ a, decode i = some a
α : Type u_1
inst✝ : Encodable α
e i : ℕ
⊢ (encode (decode e)).predO = some i → ∃ a, decode i = some a