proposition: Lemma vec_to_list_drop_lookup {A n} (v : vec A n) (i : fin n) : drop i v = v !!! i :: drop (S i) v.
proof: Proof. induction i as [|?? IHi]; inv_vec v; simpl; intros; [done | by rewrite IHi]. Qed.
imports: stdpp(countable) stdpp(options)