proposition: Lemma app_left_marker u ls : u ++ [⦇] = ⦇ :: rev (map encode_symbol ls) -> u = [] /\ ls = [].
proof: Proof. move: u ls => [|c u] [|l ls]. - done. - by move=> /(@app_inj_tail nat _ (_ :: _)) []. - by case: u. - move=> /(@app_inj_tail nat _ (_ :: _)) []. by case: l. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability(StringRewriting.Reductions.SBTM_HALT_to_SR) PeanoNat Lia List ssreflect ssrbool ssrfun