proposition: Fact bsm_progress_POP_any P i x p q b ll v st : (i,POP x p q::nil) <sc P -> v#>x = b::ll -> p = 1+i -> P // (1+i,v[ll/x]) ->> st -> P // (i,v) -+> st.
proof: Proof. destruct b; intros H1 H2 H3; subst; eauto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss)