proposition: Lemma test h1 h2 h3 x (v1 v2 : nat) : h3 = h2 -> v1 = v2 -> h1 :+ (x :-> v1) :+ h3= h2 :+ h1 :+ (x :-> v2).
proof: Proof. by move=>H1 H2; heap_congr. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep