proposition: Lemma cexit1 h1 h2 h : h1 = h2 -> h1 \+ h = h \+ h2.
proof: Proof. by move=>->; rewrite joinC. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)