no goals
α : Type u_2
β : Type u_1
γ : Type ?u.311399
σ : Type u_3
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ List.foldr (fun b s => g (a, b, s).fst (a, b, s).snd.fst :: (a, b, s).snd.snd) [] (f a) = List.map (g a) (f a)
induction f a <;> simp [*]