fact: Definition throw_prog : prog throw_pre A := fun i _ _ y m => m = i /\ y = @Exn A e.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)