proposition: Lemma vec_append_const (c : nat) n m : Vector.append (Vector.const c n) (Vector.const c m) = Vector.const c (n + m).
proof: Proof. elim: n. { done. } 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