cases (decode e : Option α) <;> simp
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ encode (decode e) = encode (encode (decode e)).predO
no goals