proposition: Lemma vec_append_inj {X n m} {v v' : Vector.t X n} {w w' : Vector.t X m} : Vector.append v w = Vector.append v' w' -> v = v' /\ w = w'.
proof: Proof. move=> /(f_equal (Vector.splitat _)). rewrite !Vector.splitat_append. by move=> [<- <-]. 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