proposition: Lemma lookUnl h1 h2 x : def (h1 :+ h2) -> look x (h1 :+ h2) = if x \in dom h1 then look x h1 else look x h2.
proof: Proof. case: h1 h2=>[|h1 H1] // [|h2 H2] //; rewrite /look /dom /union2. case: ifP=>D //= _; case: ifP=>E1; last first. - by rewrite fnd_fcat; case: ifP=>// E2; rewrite fnd_supp ?E1 // fnd_supp ?E2. suff E2: x \notin supp h2 by rewrite fnd_fcat (negbTE E2). by case: disjP D E1=>// H _; apply: H. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep