fact: Example ex3 h1 h3 x1 x2 (d1 d2 d3 d4 : nat) : def ((h3 :+ (x1 :-> d1)) :+ h1 :+ (x2 :-> d2)) -> (h3 :+ (x1 :-> d1)) :+ h1 :+ (x2 :-> d2) = (x2 :-> d3) :+ h3 :+ (x1 :-> d4) -> d1 = d4 /\ d2 = d3 /\ h1 = empty.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq eqtype) LemmaOverloading(prelude prefix heaps terms)