proposition: Lemma updUnl h1 h2 x d : upd (h1 :+ h2) x d = if x \in dom h1 then upd h1 x d :+ h2 else h1 :+ upd h2 x d.
proof: Proof. case: h1 h2=>[|h1 H1][|h2 H2] //; case: ifP=>H //; rewrite /upd /union2; case: decP=>// H3; case: ifP=>D //. - rewrite disjC disj_ins disjC D. case: disjP D=>//; move/(_ _ H)=>H4 _; rewrite H4. by apply/heapE; rewrite fcat_inss. - by rewrite disjC disj_ins disjC D andbF. - rewrite disj_ins D H /=; apply/heapE. rewrite (@fcatC _ _ h1) // (@fcatC _ _ h1). - by rewrite fcat_inss // H. by rewrite disj_ins H D. by rewrite disj_ins D andbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep