proposition: Lemma ptr_pf A x (v : A) : axiom (ptr_tag (x :-> v)) [:: x].
proof: Proof. rewrite /axiom /= defPt => D; split=>//. by move=>y; rewrite inE; move/eqP=>->; rewrite domPt inE /= eq_refl D. Qed.
imports: mathcomp(ssreflect ssrbool seq eqtype) LemmaOverloading(heaps)