proposition: Fact bsm_steps_POP_any_inv a P i x p q b ll v st : (i,POP x p q::nil) <sc P -> v#>x = b::ll -> p = 1+i -> st <> (i,v) -> P // (i,v) -[a]-> st -> { b | b < a /\ P // (1+i,v[ll/x]) -[b]-> st }.
proof: Proof. intros. destruct b. + apply bsm_steps_POP_1_inv with p q; auto. + apply bsm_steps_POP_0_inv with i q; subst; auto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss)