fact: Example ex1 x h (v1 v2:nat): def (x :-> v1 :+ h) -> x :-> v1 :+ h = x :-> v2 -> if v1 == v2 then true else false.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq eqtype) LemmaOverloading(prelude prefix xfind heaps terms)