fact: Definition logvar {B A} (G : A -> Type) (s : forall x : A, spec (G x) B) : spec {x : A & G x} B := fun '(existT x g) => s x g.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)