simp[encodeDecode, encode_decode_subtype]
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ encodeDecode { x // P x } e = (decode e).bind fun a => if P a then some (encode a) else none
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ (encode ((decode e).bind fun a => if P a then some a else none)).predO =
    (decode e).bind fun a => if P a then some (encode a) else none