proposition: Lemma st_sup_has_spec' u : st_sup' u \In has_spec.
proof: Proof. move=>g i p Vi. have J : i \In pre_of (st_sup' u). - by move=>_ [e][->]; case: e=>e P; case: (P _ _ p Vi). exists J=>y m /= [e][[[e1 P]]][/= E He1] H; subst e1. case: (P _ _ p Vi)=>Hi; apply. set I' := (X in prog_of e _ Vi X) in H. by rewrite (pf_irr Hi I'). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)