fact: Definition f' (e : lat) := sup [Pred t : lat | exists e', e' <== e /\ t = f e'].
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)