exact option_bind (Primrec.decode.comp $ snd.comp fst)
  (by apply to₂'; rw[casesOn_eq_uncurry]
      apply list_casesOn (fst.comp snd) (Primrec.const _)
        (by apply to₂'; simp[Function.uncurry]; rw[casesOn_eq_uncurry]
            apply list_casesOn (snd.comp $ snd.comp fst) (const _)
              (by unfold Function.uncurry
                  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₂ (Primrec.decodeZipWithRec f)
no goals