proposition: Fact vec_head_tail n (v : vec (S n)) : v = vec_head v ## vec_tail v.
proof: Proof. apply (vec_head_tail_prop v). Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)