proposition: Fact vec_pos0 n (v : vec (S n)) : vec_pos v pos0 = vec_head v.
proof: Proof. rewrite (vec_head_tail v). reflexivity. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)