proposition: Lemma try_case_pf A B i (s1 : A -> ST B) (s2 : exn -> ST B) r p (e : try_form i s1 s2 r p) : p -> vrf i (try e s1 s2) r.
proof: Proof. by case:e=>[?]; apply. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)