let F : α → Option (List γ) := fun a => List.recOn (f a) (some []) (fun b _ ih => (g a b).bind $ fun c => ih.map $ fun l => c :: l)
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
⊢ Primrec fun a => mapM' (g a) (f a)
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
F : α → Option (List γ) :=
  fun a => List.recOn (f a) (some []) fun b x ih => (g a b).bind fun c => Option.map (fun l => c :: l) ih
⊢ Primrec fun a => mapM' (g a) (f a)