proposition: Lemma wr_red w t : KOSBTM.wr w (conv_tape [| t |]) = conv_tape [| TM.wr w t |].
proof: Proof. unfold conv_tape. cbn. destruct t, w; reflexivity. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes Undecidability.Shared.Libs.PSL.Vectors.Vectors