proposition: Fact sss_compute_stop P st1 st2 : out_code (fst st1) P -> P // st1 ->> st2 -> st1 = st2.
proof: Proof. intros H1 (k & H2); revert H2; apply sss_steps_stop; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)