proposition: Lemma vector_inv_back {X n} (v : Vector.t X (S n)) E : { '(x, v') : X * Vector.t X n | v = Vector.cast (Vector.append v' (x ## vec_nil)) E }.
proof: Proof. destruct E. destruct (Vector.splitat n v) eqn:E. eexists (vec_head t0, t). erewrite <- Vector.append_splitat. 1: now rewrite cast_eq_refl. rewrite E. f_equal. eapply (Vector.caseS' t0). cbn. intros h. eapply Vector.case0. reflexivity. 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)