proposition: Fact subcode_sss_step P Q st1 st2: P <sc Q -> P // st1 :1> st2 -> Q // st1 :1> st2.
proof: Proof. destruct P as (n1,c1). destruct Q as (n2,c2). simpl. intros (l & r & H1 & H2) H3. destruct H3 as (q & ll & i & rr & d1 & H3 & H4 & H5). inversion H3; subst. exists n2, (l++ll), i, (rr++r), d1; repeat split; auto. f_equal; solve list eq. f_equal; rew length; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)