rcases List.mapM' (decode : ℕ → Option (SubWType β s)) (Denumerable.ofNat (List ℕ) e.unpair.2) with (_ | w) <;> simp
case succ.e_a.h
α : 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 : ℕ
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)) =
    (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)
case succ.e_a.h.some
α : 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 : ℕ
a : α
w : List (SubWType β s)
⊢ 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)) w) =
    Option.map (fun v => f a v)
      (if w.length = Fintype.card (β a) then
        some (List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w)
      else none)