fact: Fixpoint vdrop {A n} (i : fin n) : vec A n → vec A (n - i) := match i in fin n return vec A n → vec A (n - i) with | 0%fin => id | FS i => vec_S_inv _ (λ _, vdrop i) end.
imports: stdpp(countable) stdpp(options)