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