proposition: Lemma lookUnr h1 h2 x : def (h1 :+ h2) -> look x (h1 :+ h2) = if x \in dom h2 then look x h2 else look x h1.
proof: Proof. by rewrite unC=>D; rewrite lookUnl. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep