proposition: Lemma vec_app_inj {X} (n m : nat) v1 v2 v2' : @vec_app X n m v1 v2 = vec_app v1 v2' -> v2 = v2'.
proof: Proof. induction v1. - now rewrite !vec_app_nil. - rewrite !vec_app_cons. intros. eapply IHv1. now eapply (f_equal (@vec_tail _ _)) in H. 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)