proposition: Lemma opn : forall (A : Type) (v : A) x h, h \In x :--> v <-> x :-> v = h.
proof: Proof. by move=>A v x h; split=>[|H]; rewrite InE /= /pts; unlock. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)