simp[Function.comp, encodeDecode_eq_encode_map_decode]
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
⊢ (Option.casesOn (Option.map SubWType.toW (decode e)) 0 fun w => encode (SubWType.ofW w) + 1) =
    encode
      ((encodeDecode (SubWType β e.unpair.1) e.unpair.2).bind fun c =>
        Option.map (fun d => d.pair c) (Option.map (fun w => (↑w).depth) (decode c)))
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
⊢ Option.rec 0 (fun val => encode (SubWType.ofW val) + 1)
      (Option.map (fun x => SubWType.toW ⟨e.unpair.1, x⟩) (decode e.unpair.2)) =
    encode ((Option.map encode (decode e.unpair.2)).bind fun a => Option.map (fun x => (↑x).depth.pair a) (decode a))