proposition: Lemma try_has_spec : try_sp \In has_spec try_s.
proof: Proof. move=>i y m; case=>[[[/= S1 [S2 S3]]]] D [h][x][j][<-][]. case: x=>[x'|e'] T1 T2; [left; exists x' | right; exists e']; exists j; by split; [apply: spec_runs T1 | apply: spec_runs T2]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)