fact: Definition heap_inv h r (f : abs_heap h r) := match f return pack_h f = h :+ r with AbsHeap h' i => i end.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq eqtype) LemmaOverloading(prelude prefix heaps terms)