proposition: Fact sss_step_in_code P st1 st2 : P // st1 :1> st2 -> in_code (fst st1) P.
proof: Proof. revert P st1 st2; intros (n,c) (i,d) st2 (q & l & ii & r & d1 & H1 & H2 & _). inversion H1; subst. inversion H2; subst. simpl; rew length; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)