proposition: Fact sss_step_subcode_inv P ii st st' : (fst st, ii::nil) <sc P -> P // st :1> st' -> ii // st -1> st'.
proof: Proof. intros H1 (k & l2 & jj & r2 & d1 & H3 & H4 & H5); subst P st. destruct H1 as (l1 & r1 & H1 & H2). simpl in H1, H2. apply list_app_inj in H1; try lia. destruct H1 as (? & H1); subst l2. inversion H1; subst jj r2; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)