proposition: Lemma throwP : Model.conseq (Model.throw_s A e) [throw_s].
proof: Proof. move=>i H D; split=>{H D} // y m [->] -> _ i1 h -> D ->. by exists empty; rewrite un0h; do !split=>//; apply: defUnr D. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)