proposition: Fact sss_steps_stop P k st1 st2 : out_code (fst st1) P -> P // st1 -[k]-> st2 -> st1 = st2.
proof: Proof. intros H1 H2. apply sss_steps_inv in H2. destruct H2 as [ [ _ ? ] | (k' & st3 & H2 & H3 & H4) ]; auto. destruct (sss_out_step_stall H1 H3). Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)