proposition: Fact in_sss_step k l i r st1 st2 : fst st1 = k+length l -> i // st1 -1> st2 -> (k,l++i::r) // st1 :1> st2.
proof: Proof. destruct st1 as (j,d); simpl; intro; subst; exists k,l,i,r,d; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)