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