case equal n i j =>
  have : Primrec (fun (v : Vector ℕ n) => if v.get i = v.get j then 1 else 0) :=
    Primrec.ite
      (Primrec.eq.comp
        (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
        (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j)))
      (_root_.Primrec.const 1)
      (_root_.Primrec.const 0)
  exact Partrec'.of_part this.to_comp.partrec
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => (v.get i).isEqNat (v.get j)
no goals