proposition: Lemma throw_coherent : coherent throw_sp.
proof: Proof. move=>p y m; split; first by case=>H ->{y}; exists m; exists H. by case=>i [H1] [<-{m}] ->{y}. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)