fact: Definition conseq A (s1 s2 : spec A) := forall i, s2.1 i -> def i -> s1.1 i /\ forall y m, s1.2 y i m -> def m -> s2.2 y i m.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)