proposition: Lemma blah2 (A : Type) (v1 v2 : A) q : def (q :-> v1) -> v1 = v2 -> q :-> v1 \In q :--> v2.
proof: Proof. by move=>D E; apply/swp; rewrite E. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)