exact (Partrec'.of_part ((Primrec.nat_add.comp
  (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
  (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j))).to_comp.partrec))
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => v.get i + v.get j
no goals