exact decode_iff.mp (encode_iff.mp $ this.of_eq $ fun e => by
  simp[encodeDecode_eq_encode_map_decode, decode_finArrow]
  rcases (decode e) with (_ | as) <;> simp [Function.comp]
  { rcases (as.toVector k) with (_ | v) <;> simp
    { simp[encode_finArrow, Function.comp] } })
σ : 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))
⊢ Primrec fun v i => f (v i)
no goals