proposition: Lemma try_dstrict : def_strict try_sp.
proof: Proof. move=>p y [i][x][h][H1][]. by case: x=>[x'|e'] H2; case/def_runs. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)