proposition: Lemma mv_red m t : KOSBTM.mv (conv_move m) (conv_tape [| t |]) = conv_tape [| TM.mv m t |].
proof: Proof. unfold conv_tape. cbn. destruct t, m; try reflexivity. all: destruct l, l0; reflexivity. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes Undecidability.Shared.Libs.PSL.Vectors.Vectors