proposition: Fact sss_step_supcode P Q st st' : P <sc Q -> in_code (fst st) P -> Q // st :1> st' -> P // st :1> st'.
proof: Proof. intros H1 H2 (k & l & ii & r & d & ? & ? & H3); subst. destruct P as (iP,cP). destruct H1 as (ll & rr & H1 & H4). simpl in H2. symmetry in H1. apply list_app_cons_eq_inv in H1. destruct H1 as [ (m & G1 & G2) | (m & G1 & G2) ]. 2: apply f_equal with (f := @length _) in G1; exfalso; revert G1; rew length; intro; lia. apply list_app_cons_eq_inv in G2. destruct G2 as [ (p & G3 & G4) | (p & G3 & G4) ]. subst; exfalso; revert H2; rew length; intro; lia. subst. apply in_sss_step; auto. revert H2; rew length; simpl; intro; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)