proposition: Lemma vec'_pos_app_right {X : Type} (n m : nat) (v : vec X n) (w : vec X m) (i : pos m) : vec_pos (v +++ w) (pos_right n i) = vec_pos w i.
proof: Proof. rewrite <- !vec_app_spec. apply vec_pos_app_right. Qed.
imports: Undecidability.StackMachines.BSM Undecidability.StackMachines.Util.BSM_computable Undecidability.TM.TM Undecidability.TM.Util.TM_facts Undecidability.TM.Util.TM_computable Undecidability.TM(TM Arbitrary_to_Binary mTM_to_TM HaltTM_1_to_HaltKOSBTM HaltKOSBTM_to_HaltBSM) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Undecidability(bsm_utils bsm_defs) Undecidability.TM.Code.Code Undecidability.TM(Single.EncodeTapes)