proposition: Lemma try_dstrict : def_strict try_prog.
proof: Proof. move=>i [Vi [Pi][E1 E2]] Vi' y[x][h][/=]. by case: x=>[x|ex] Eh; case=>Ph /dstr_st. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)