proposition: Lemma dom_notin_notin h1 h2 x : def (h1 :+ h2) -> x \notin dom (h1 :+ h2) -> x \notin dom h1.
proof: Proof. by move=>D; rewrite domUn inE /= negb_and negb_or /= D; case/andP. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep