proposition: Lemma decompose_vec2 {X : Type} (v : vec X 2) : v = vec_head v ## vec_head (vec_tail v) ## vec_nil.
proof: Proof. by rewrite [LHS](vec_head_tail v) [in LHS](vec_head_tail (vec_tail v)) [in LHS](vec_0_nil (vec_tail (vec_tail v))). Qed.
imports: PeanoNat Lia List Undecidability.MinskyMachines(MM MM_sss) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) ssreflect ssrbool ssrfun