proposition: Fact sss_stall_step_0 ii P q st st' : (fst st,ii::nil) <sc P -> sss_stall ii st -> P // st -[q]-> st' -> q = 0 /\ st = st'.
proof: Proof. intros H1 H2. generalize (sss_stall_step_stall H1 H2). intros H3 H4. apply sss_steps_inv in H4. destruct H4 as [ | (k & st2 & _ & H5 & _) ]; auto. contradict H5; apply H3. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)