proposition: Lemma doAct_canonize_tape {t1 t2} a d : canonize_tape t1 = canonize_tape t2 -> canonize_tape (TM_facts.doAct t1 (Some a, encode_direction d)) = canonize_tape (TM_facts.doAct t2 (Some a, encode_direction d)).
proof: Proof. move: d t1 t2. move=> [] [ | ?? | ?? | [|??]?[|??] ] [ | ?? | ?? | [|??]?[|??] ] /=; cbn; congruence. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun