proposition: Lemma sc_skipn {X : Type} k i x (P Q : list X) : (i, x::P) <sc (i, skipn k Q) -> (k + i, x::P) <sc (i, Q).
proof: Proof. intros [l [r [??]]]. destruct l as [|??]; [|cbn in *; lia]. eexists (firstn k Q), r. split. - transitivity (firstn k Q ++ skipn k Q); [now rewrite firstn_skipn|]. now rewrite H. - rewrite firstn_length_le; [lia|]. revert Q H. induction k as [|k IH]; [lia|]. intros [|y Q]; [easy|]. + intros H%IH. cbn. lia. Qed.
imports: Undecidability.TM.KOSBTM.KOSBTM Undecidability.Shared.Libs.PSL.Vectors.FinNotation Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.Shared.Libs.PSL.EqDec List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(bsm_defs)