rcases s with (_ | s) <;> simp
α : 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 γ → γ
x : σ
s e : ℕ
⊢ Nat.rec none
      (fun n n_ih =>
        (decode e.unpair.1).bind fun a =>
          Option.map (fun v => f x a v)
            ((mapM'
                  (fun c =>
                    (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range (s.pair e))).getI
                      (n.pair c))
                  (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
              fun l => if l.length = Fintype.card (β a) then some l else none))
      s =
    Nat.rec none
      (fun n n_ih =>
        (decode e.unpair.1).bind fun a =>
          Option.map (fun v => f x a v)
            ((mapM' (elimDecode β (f x) n) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
              if l.length = Fintype.card (β a) then some l else none))
      s
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 γ → γ
x : σ
e s : ℕ
⊢ ((decode e.unpair.1).bind fun a =>
      Option.map (fun v => f x a v)
        ((mapM'
              (fun c =>
                (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                  (s.pair c))
              (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
          fun l => if l.length = Fintype.card (β a) then some l else none)) =
    (decode e.unpair.1).bind fun a =>
      Option.map (fun v => f x a v)
        ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
          if l.length = Fintype.card (β a) then some l else none)