proposition: Lemma vec_to_list_lookup_middle {A n} (v : vec A n) (l k : list A) x : vec_to_list v = l ++ x :: k → ∃ i : fin n, l = take i v ∧ x = v !!! i ∧ k = drop (S i) v.
proof: Proof. intros H. rewrite <-(vec_to_list_to_vec l), <-(vec_to_list_to_vec k) in H. rewrite <-vec_to_list_cons, <-vec_to_list_app in H. pose proof (vec_to_list_inj1 _ _ H); subst. apply vec_to_list_inj2 in H; subst. induction l as [|?? IHl]; simpl. - eexists 0%fin. simpl. by rewrite vec_to_list_to_vec. - destruct IHl as [i ?]. exists (FS i). simpl. intuition congruence. Qed.
imports: stdpp(countable) stdpp(options)