proposition: Lemma vec_append_splitat {X n m} (v : Vector.t X (n + m)) : v = Vector.append (fst (Vector.splitat _ v)) (snd (Vector.splitat _ v)).
proof: Proof. apply: Vector.append_splitat. by case: (Vector.splitat n v). Qed.
imports: Undecidability(TM.TM) Undecidability.MinskyMachines(MM MMA MMA.mma_defs Util.MMA_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) List PeanoNat Lia Relations ssreflect