proposition: Fact subcode_sss_step_inv P Q st1 st2 : P <sc Q -> in_code (fst st1) P -> Q // st1 :1> st2 -> P // st1 :1> st2.
proof: Proof. revert P Q st1 st2; intros (nP,cP) (nQ,cQ) (i,d) st; simpl. intros (l & r & H1 & H2) H3 (q & ll & ii & rr & d1 & H4 & H5 & H6). inversion H4; subst. inversion H5; subst. clear H4 H5. apply list_app_cons_eq_inv in H7. destruct H7 as [ (m & Hm1 & Hm2) | (m & Hm1 & Hm2) ]. apply list_app_cons_eq_inv in Hm2. destruct Hm2 as [ (p & Hp1 & Hp2) | (p & Hp1 & Hp2) ]. + apply f_equal with (f := @length _) in Hm1. apply f_equal with (f := @length _) in Hp1. revert Hm1 Hp1; rew length; intros; lia. + subst cP; apply in_sss_step; auto. simpl; subst; rew length; lia. + apply f_equal with (f := @length _) in Hm1. apply f_equal with (f := @length _) in Hm2. revert Hm1 Hm2; rew length; intros; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)