proposition: Fact sss_out_step_stall P st : out_code (fst st) P -> sss_step_stall P st.
proof: Proof. revert P st; intros (n,code) (i,st). intros H1 st' (k & l & ii & r & d1 & H2 & H3 & H4). inversion H2; inversion H3; subst. simpl in H1. revert H1; rew length; intros []; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)