proposition: Lemma domUn h1 h2 : dom (h1 :+ h2) =i [pred x | def (h1 :+ h2) && (x \in [predU dom h1 & dom h2])].
proof: Proof. case: h1 h2 =>[|h1 H1] // [|h2 H2] // x; rewrite /dom /union2. by case: ifP=>// E; rewrite supp_fcat. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep