proposition: Lemma vec_to_list_take_drop_lookup {A n} (v : vec A n) (i : fin n) : vec_to_list v = take i v ++ v !!! i :: drop (S i) v.
proof: Proof. rewrite <-(take_drop i v) at 1. by rewrite vec_to_list_drop_lookup. Qed.
imports: stdpp(countable) stdpp(options)