proposition: Fact sss_steps_S_inv' P st1 st3 k : P // st1 -[S k]-> st3 -> exists st2, P // st1 :1> st2 /\ P // st2 -[k]-> st3.
proof: Proof. intros H. inversion H; subst. exists st2; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)