fact: Definition pts_inv x A (v :A) r (f : abs_pts x v r) := match f return (pack_h f = x:->v:+r) with (AbsPts p i) => i end.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq eqtype) LemmaOverloading(prelude prefix heaps terms)