proposition: Lemma eqexnP : Equality.axiom eqexn.
proof: Proof. move=>[x][y]//=; case: eqP=>[->|*];constructor=>//. by move=>[*]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)