fact: Parameter vrf_throw : forall A e i (Q : post A), (valid i -> Q (Exn e) i) -> vrf i (throw e) Q.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)