fact: Definition hstep_bnd A B i (s : A -> spec B) r p (e : bnd_form i s r p) : p -> verify (bind_s e s) i r := let: BndForm _ pf := e in pf.
imports: mathcomp(ssreflect ssrbool ssrfun) LemmaOverloading(heaps rels stmod stsep stlog)