simp
case zero
α : 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 : ℕ
⊢ Option.map
      (elim' γ
        (fun x =>
          match x with
          | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
        0)
      (decode e) =
    Nat.casesOn 0 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)
no goals