simp[SubWType.decode_succ, Option.map_bind', decode_list, Function.comp, List.mapM'_option_map]
case succ
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
σ : Type u_3
γ : Type u_4
f : α → List γ → γ
e s : ℕ
⊢ Option.map
      (elim' γ
        (fun x =>
          match x with
          | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
        (s + 1))
      (decode e) =
    Nat.casesOn (s + 1) none fun s =>
      (decode e.unpair.1).bind fun a =>
        Option.map (fun v => f a v)
          ((mapM'
                (fun e =>
                  Option.map
                    (elim' γ
                      (fun x =>
                        match x with
                        | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
                      s)
                    (decode e))
                (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
            fun l => if l.length = Fintype.card (β a) then some l else none)
case succ
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
σ : Type u_3
γ : Type u_4
f : α → List γ → γ
e s : ℕ
⊢ ((decode e.unpair.1).bind fun a =>
      (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun a_1 =>
        Option.map
          (fun x =>
            elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (s + 1)
              (ofWType (WType.mk a fun b => ↑(x.get (fintypeEquivFin b))) (s + 1) ⋯))
          (List.toVector (Fintype.card (β a)) a_1)) =
    (decode e.unpair.1).bind fun a =>
      (Option.map (fun bs => List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) bs)
            (mapM' (fun a => decode a) (Denumerable.ofNat (List ℕ) e.unpair.2))).bind
        fun a_1 => Option.map (fun v => f a v) (if a_1.length = Fintype.card (β a) then some a_1 else none)