proposition: Lemma st_supM u e : (forall e1, e1 \In u -> e1 <== e) -> st_sup u <== e.
proof: Proof. case: e=>p e S D F R. have J : p <== pre_sup u. - by move=>/= x Px e' pf; case: (R _ pf)=>/= + _; apply. exists J=>i V P y m [e0][H0 Hm]. case: (R _ H0)=>/= Hx; apply. by rewrite (pf_irr (Hx i P) (pre_sup_leq H0 (J i P))). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)