proposition: Lemma eqexnP : Equality.axiom eqexn.
proof: Proof. by move=>[x][y]/=; case: eqP=>[->|*]; constructor=>//; case. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)