proposition: Fact vec_cons_inv n x y (v w : vec n) : x ## v = y ## w -> x = y /\ v = w.
proof: Proof. intros H1; generalize H1; intros H2. apply f_equal with (f := @vec_head _) in H1. apply f_equal with (f := @vec_tail _) in H2. auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)