proposition: Fact sss_steps_stall_inv P p s1 s2 : sss_step_stall P s1 -> P // s1 -[p]-> s2 -> p = 0 /\ s1 = s2.
proof: Proof. intros H; induction 1 as [ | p st1 st2 st3 H1 ]; auto. apply H in H1; destruct H1. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)