proposition: Fact bsm_steps_POP_0_inv a P i x p q ll v st : (i,POP x p q::nil) <sc P -> v#>x = Zero::ll -> st <> (i,v) -> P // (i,v) -[a]-> st -> { b | b < a /\ P // (p,v[ll/x]) -[b]-> st }.
proof: Proof. intros H1 H2 H3 H4. apply sss_steps_inv in H4. destruct H4 as [ (_ & ?) | (b & H4) ]; subst. 1: destruct H3; auto. exists b. destruct H4 as (st2 & ? & H4 & H5); subst. split; try lia. apply sss_step_subcode_inv with (1 := H1) in H4. inversion H4; subst; try mydiscr; myinj. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss)