proposition: Lemma vec_eq {A n} (v w : vec A n) : (∀ i, v !!! i = w !!! i) → v = w.
proof: Proof. vec_double_ind v w; [done|]. intros n v w IH x y Hi. f_equal. - apply (Hi 0%fin). - apply IH. intros i. apply (Hi (FS i)). Qed.
imports: stdpp(countable) stdpp(options)