{ by_cases ha : P a <;> simp[*] }
case some
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
a : α
⊢ (encode (if P a then some a else none)).predO = if P a then some (encode a) else none
no goals