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