proposition: Fact sss_stall_step_stall ii P st : (fst st,ii::nil) <sc P -> sss_stall ii st -> sss_step_stall P st.
proof: Proof. intros H1 H2 st' H. apply sss_step_subcode_inv with (1 := H1) in H. revert H; apply H2. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)