proposition: Fact vec_eq_dec n (u v : vec n) : { u = v } + { u <> v }.
proof: Proof. Proof using eq_X_dec. apply vec_eq_dec_pos; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)