fact: Fixpoint vtake {A n} (i : fin n) : vec A n → vec A i := match i in fin n return vec A n → vec A i with | 0%fin => λ _, [#] | FS i => vec_S_inv _ (λ x v, x ::: vtake i v) end.
imports: stdpp(countable) stdpp(options)