fact: Definition try_pre_proj i : i \In try_pre -> i \In pre_of e := fun '(ex_intro _ (ex_intro p _)) => p.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)