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)
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => (v.get i).isEqNat (v.get j)
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
this : Primrec fun v => if v.get i = v.get j then 1 else 0
⊢ Partrec' ↑fun v => (v.get i).isEqNat (v.get j)