simp[encode_finArrow, Function.comp]
case some.some
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
as : List α
v : Vector α k
⊢ encode (Option.map (fun l => List.map f l) (decode (encode ((Equiv.vectorEquivFin α k) v)))) =
    (encode fun i => f ((Equiv.vectorEquivFin α k) v i)) + 1
no goals