proposition: Lemma current_red t : KOSBTM.curr (conv_tape [| t |]) = TM.current t.
proof: Proof. destruct t; reflexivity. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes Undecidability.Shared.Libs.PSL.Vectors.Vectors