simp[List.getI_map_range _ this]
α : 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 : ℕ
a : α
c : ℕ
hc : c ∈ Denumerable.ofNat (List ℕ) e.unpair.2
this : s.pair c < (s + 1).pair e
⊢ (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair c) =
    elimDecode β (f x) s c
no goals