proposition: Fact subcode_sss_step_inv_1 P i st1 st2 : (fst st1,i::nil) <sc P -> P // st1 :1> st2 -> i // st1 -1> st2.
proof: Proof. revert P st1; intros (j,cj) (n,d) H1 H2. apply subcode_sss_step_inv with (1 := H1) in H2. 2: simpl; lia. destruct H2 as (q & l & ii & r & d1 & H2 & H3 & H4). inversion H3; subst n d1; auto. eq goal H4; f_equal. inversion H2. destruct l as [ | ? [ | ] ]; try discriminate. inversion H5; subst; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)