proposition: Fact vec_pos_ext n (v w : vec n) : (forall p, vec_pos v p = vec_pos w p) -> v = w.
proof: Proof. revert v w; induction n as [ | n IHn ]; intros v w H. 1: rewrite (vec_0_nil v), (vec_0_nil w); auto. revert H; rewrite (vec_head_tail v), (vec_head_tail w); f_equal. intros H; f_equal. + apply (H pos0). + apply IHn. intros p; apply (H (pos_nxt p)). Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)