proposition: Lemma dom_in_notin h1 h2 x : def (h1 :+ h2) -> x \in dom h1 -> x \notin dom h2.
proof: Proof. by case: defUn=>// D1 D2 H _; apply: H. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep