proposition: Lemma st_sup_coherent u : coherent (st_sup' u).
proof: Proof. move=>r x m; split. - case=>_ [[_]][[_]][[_]][[]][p] M S H [->] P -> -> -> /=. case/M=>i [pf] H1. exists i; exists pf; exists (p (single (bound pf)) x m). split=>//; do 3![eexists _; split=>//]. by exists (STprog M S H). case=>i [pf][_][[_]][[_]][[_]][[]][p] M D H [->] P -> -> -> /= E. have: exists i, exists pf : i \In id_val r, m \In p (single (bound pf)) x. - by exists i; exists pf. move/M=>H3; exists (p r x m); split=>//; do 3![eexists _; split=>//]. by exists (STprog M D H). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)