proposition: Lemma pts_pf A hs xs1 xs2 x (d : A) (xs : xfind xs1 xs2 x): invariant (Context hs xs1) (Context hs xs2) [:: Pts x (dyn d)] (pts_tag (xuntag xs :-> d)).
proof: Proof. case: xs=>[p /= [H P]]; split; first by rewrite /= H. - by split; [apply: prefix_refl|]. by apply/andP; rewrite /= (onth_size H). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq eqtype) LemmaOverloading(prelude prefix xfind heaps terms)