rcases (decode e.unpair.2 : Option (β a)) with (_ | b) <;> simp[*]
case some
α✝ : Type u_1
inst✝³ : Encodable α✝
α : Type u_1
P : α → Prop
inst✝² : Encodable α
inst✝¹ : DecidablePred P
β : α → Type u_2
inst✝ : (a : α) → Encodable (β a)
e : ℕ
a : α
ha : decode e.unpair.1 = some a
⊢ (encode (Option.map (Sigma.mk a) (decode e.unpair.2))).predO =
    Option.map (fun b => (encode a).pair b) (encode (decode e.unpair.2)).predO
no goals