proposition: Lemma Shift_steps_local (rs : list sig) : Shift_steps rs <= 4 + 4 * length rs.
proof: Proof. induction rs; cbn in *. - lia. - destruct (f a); lia. Qed.
imports: Undecidability(TM.Util.Prelim) Undecidability(TM.Basic.Mono) Undecidability(TM.Combinators.Combinators) Undecidability(TM.Compound.TMTac) Undecidability(TM.Compound.Multi) Coq(FunInd) Coq(Recdef)