proposition: Fact sss_steps_trans P n m st1 st2 st3 : P // st1 -[n]-> st2 -> P // st2 -[m]-> st3 -> P // st1 -[n+m]-> st3 .
proof: Proof. intros H; revert H st3. induction 1 as [ | ? ? st2 ]; simpl; intros; auto. constructor 2 with st2; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)