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