fact: Definition coherent (e : prog) := forall p x m, m \In e p x <-> exists i, exists pf : i \In id_val p, m \In e (single (bound pf)) x.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)