fact: Definition lolli (p : _ -> Prop) q i m := forall i1 h, i = i1 :+ h -> def i -> p i1 -> exists m1, m = m1 :+ h /\ def m /\ q i1 m1.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)