proposition: Fact sss_steps_stall k P st st' : out_code (fst st) P -> P // st -[k]-> st' -> k = 0 /\ st = st'.
proof: Proof. destruct P; simpl. intros H1 H2. apply sss_steps_inv in H2. destruct H2 as [ (? & ?) | (m & st2 & ? & H2 & _) ]; auto. apply sss_out_step_stall in H2; try red; tauto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)