apply option_map (list_get?.comp (snd.comp $ fst.comp $ fst.comp fst)
  (Primrec₂.natPair.comp
    (snd.comp $ unpair.comp $ pred.comp $ fst.comp $ unpair.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)
    (snd.comp $ unpair.comp $ pred.comp $ snd.comp $ unpair.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)))
  (list_cons.comp₂
    (hf.comp₂
      (fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ Primrec₂.left)
      (Primrec₂.pair.comp₂
        (fst.comp₂ $ snd.comp₂ $ fst.comp₂ Primrec₂.left)
        (fst.comp₂ $ snd.comp₂ Primrec₂.left)))
    (option_iget.comp₂ Primrec₂.right))
α : 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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec₂ fun a a_1 =>
    (fun head tail =>
        Option.map (fun cs => f a.1.1.1.1 (a.2.1, head) :: cs.iget)
          (a.1.1.2.get? ((a.1.1.1.2.unpair.1 - 1).unpair.2.pair (a.1.1.1.2.unpair.2 - 1).unpair.2)))
      a_1.1 a_1.2
no goals