∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] {c : α → Nat.Partrec.Code},
  Primrec c →
    ∀ {z : α → σ},
      Primrec z →
        ∀ {s : α → σ},
          Primrec s →
            ∀ {l : α → σ},
              Primrec l →
                ∀ {r : α → σ},
                  Primrec r →
                    ∀ {pr : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
                      Primrec₂ pr →
                        ∀ {co : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
                          Primrec₂ co →
                            ∀ {pc : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
                              Primrec₂ pc →
                                ∀ {rf : α → Nat.Partrec.Code × σ → σ},
                                  Primrec₂ rf →
                                    have PR := fun a cf cg hf hg => pr a (cf, cg, hf, hg);
                                    have CO := fun a cf cg hf hg => co a (cf, cg, hf, hg);
                                    have PC := fun a cf cg hf hg => pc a (cf, cg, hf, hg);
                                    have RF := fun a cf hf => rf a (cf, hf);
                                    have F := fun a c =>
                                      Nat.Partrec.Code.recOn c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a);
                                    Primrec fun a => F a (c a)