proposition: Lemma updUnr h1 h2 x d : upd (h1 :+ h2) x d = if x \in dom h2 then h1 :+ upd h2 x d else upd h1 x d :+ h2.
proof: Proof. by rewrite unC updUnl (unC h1) (unC h2). Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep