simp [F, e]
α : 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
this : Primrec F
e :
  ∀ (k : β → Option γ) (bs : List β),
    (List.recOn bs (some []) fun b x ih => (k b).bind fun c => Option.map (fun l => c :: l) ih) = mapM' k bs
⊢ ∀ (n : α), F n = mapM' (g n) (f n)
no goals