proposition: Lemma retP : Model.conseq (Model.ret_s x) [ret_s].
proof: Proof. move=>i /= H1 D1; split=>// y m [->] -> _ i1 i2 -> D ->. by exists empty; rewrite un0h (defUnr D). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)