simp[Option.map_eq_bind, Function.comp]
case cons
α : 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
k : β → Option γ
head✝ : β
tail✝ : List β
tail_ih✝ :
  (List.recOn tail✝ (some []) fun b x ih => (k b).bind fun c => Option.map (fun l => c :: l) ih) = mapM' k tail✝
⊢ ((k head✝).bind fun a => Option.map (fun l => a :: l) (mapM' k tail✝)) =
    (k head✝).bind fun __do_lift => (mapM' k tail✝).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1)
no goals