rw[casesOn_eq_uncurry]
case hf
α : 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 p =>
    List.casesOn p.2.1 (some []) fun a x =>
      List.casesOn p.2.2 (some []) fun b x =>
        Option.map (fun cs => f p.1.1.1 (a, b) :: cs.iget)
          (p.1.2.get? (encode (p.1.1.2.unpair.1.pred.unpair.2, p.1.1.2.unpair.2.pred.unpair.2)))
case hf
α : 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 x =>
    List.casesOn x.2.1 (some []) fun a as =>
      Function.uncurry
        (fun head tail =>
          (fun a x_1 =>
              List.casesOn x.2.2 (some []) fun b x_2 =>
                Option.map (fun cs => f x.1.1.1 (a, b) :: cs.iget)
                  (x.1.2.get? (encode (x.1.1.2.unpair.1.pred.unpair.2, x.1.1.2.unpair.2.pred.unpair.2))))
            head tail)
        (a, as)