proposition: Lemma get_symbol_canonize_tape {t1 t2} : canonize_tape t1 = canonize_tape t2 -> get_symbol (TM.current t1) = get_symbol (TM.current t2).
proof: Proof. move: t1 t2 => [ | ?? | ?? | ???] [] > /=; congruence. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun