fact: Example triggered A (x1 x2 x3 : ptr) (v1 v2 v3 : A) (h1 h2 : heap) : def (h1 :+ (x1 :-> v1 :+ x2 :-> v2) :+ (h2 :+ x3 :-> v3)) -> (x1 != x3) && (x2 != x3) && (x1 != x2).
imports: mathcomp(ssreflect ssrbool seq eqtype) LemmaOverloading(heaps)