proposition: Fact vec_one_fst n : @vec_one (S n) pos0 = 1##vec_zero.
proof: Proof. apply vec_pos_ext; intros p; pos_inv p; rew vec. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)