proposition: Lemma blah (A : Type) (p : ptr) (l : A) : def (p :-> l) -> (p :-> l) \In p :--> l.
proof: Proof. by move=>H; apply/swp. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)