proposition: Lemma noalias h1 h2 x1 x2 : x1 \in dom h1 -> x2 \in dom h2 -> def (h1 :+ h2) -> x1 != x2.
proof: Proof. by case: defUn=>// H1 H2 H; move/H; case: eqP=>// ->; move/negbTE=>->. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep