proposition: Fact sss_compute_progress_trans P st1 st2 st3 : P // st1 ->> st2 -> P // st2 -+> st3 -> P // st1 -+> st3.
proof: Proof. intros (i & H1) (j & ? & H2); exists (i+j); split; try lia; revert H1 H2; apply sss_steps_trans. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)