proposition: Lemma throw_has_spec : throw_sp \In has_spec throw_s.
proof: Proof. by move=>i y m; case=>/= T [-> ->]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)