fact: Example ex2 A (x1 x2 : ptr) (v1 v2 : A) (h1 h2 : heap) : def (h1 :+ x1 :-> 1 :+ (x2 :-> 3 :+ empty)) -> if x2 \in dom (h1 :+ x1 :-> 1 :+ (x2 :-> 3 :+ empty)) then 1 == 1 else 1 == 0.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype) LemmaOverloading(heaps)