proposition: Fact sss_steps_plus_inv P n m st1 st3 : P // st1 -[n+m]-> st3 -> exists st2, P // st1 -[n]-> st2 /\ P // st2 -[m]-> st3.
proof: Proof. revert st1 st3; induction n as [ | n IHn ]; intros s t. exists s; split; auto; constructor. inversion 1; subst. apply IHn in H2; destruct H2 as (st & ? & ?). exists st; split; auto. constructor 2 with st2; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)