rw[Encodable.decode_ofEquiv equiv_succ, equiv_succ]
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ decode e =
    Option.map (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯)
      ((decode e.unpair.1).bind fun a => Option.map (Sigma.mk a) (decode e.unpair.2))
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ Option.map
      (⇑{
            toFun := fun x =>
              match x with
              | ⟨t, h⟩ =>
                WType.casesOn (motive := fun x => x.depth ≤ s + 1 → (a : α) × (β a → SubWType β s)) t
                  (fun a f h => ⟨a, fun b => ⟨f b, ⋯⟩⟩) h,
            invFun := fun x =>
              match x with
              | ⟨a, f⟩ => ofWType (WType.mk a fun b => ↑(f b)) (s + 1) ⋯,
            left_inv := ⋯, right_inv := ⋯ }.symm)
      (decode e) =
    Option.map (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯)
      ((decode e.unpair.1).bind fun a => Option.map (Sigma.mk a) (decode e.unpair.2))